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

Theorem jctr 542
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 22 . 2  |-  ( ph  ->  ph )
2 jctl.1 . 2  |-  ps
31, 2jctir 538 1  |-  ( ph  ->  ( ph  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  mpanl2  681  mpanr2  684  bm1.1OLD  2428  brprcneu  5703  mpt2eq12  6165  tfr3  6877  oaabslem  7101  omabslem  7104  isinf  7545  pssnn  7550  uzindi  11822  drsdirfi  15127  ga0  15835  lbsext  17263  lindfrn  18269  fbssint  19430  filssufilg  19503  neiflim  19566  lmmbrf  20792  caucfil  20813  constr2spth  23518  constr2pth  23519  constr3lem4  23552  sspid  24142  onsucsuccmpi  28308  diophun  29135  eldioph4b  29173  dvsid  29628  dvsef  29629  cnfex  29773  ige2m2fzo  30243  un10  31544  lhpexle1  33675
  Copyright terms: Public domain W3C validator