MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jctr Structured version   Unicode version

Theorem jctr 527
Description: Inference conjoining a theorem to the right of a consequent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.)
Hypothesis
Ref Expression
jctl.1  |-  ps
Assertion
Ref Expression
jctr  |-  ( ph  ->  ( ph  /\  ps ) )

Proof of Theorem jctr
StepHypRef Expression
1 id 20 . 2  |-  ( ph  ->  ph )
2 jctl.1 . 2  |-  ps
31, 2jctir 525 1  |-  ( ph  ->  ( ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mpanl2  663  mpanr2  666  bm1.1  2420  brprcneu  5713  mpt2eq12  6126  tfr3  6652  oaabslem  6878  omabslem  6881  isinf  7314  pssnn  7319  uzindi  11310  drsdirfi  14385  ga0  15065  lbsext  16225  fbssint  17860  filssufilg  17933  neiflim  17996  lmmbrf  19205  caucfil  19226  constr2spth  21590  constr2pth  21591  constr3lem4  21624  sspid  22214  onsucsuccmpi  26158  diophun  26786  eldioph4b  26826  lindfrn  27223  dvsid  27480  dvsef  27481  cnfex  27630  un10  28801  lhpexle1  30706
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator