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  2444  brprcneu  5850  mpt2eq12  6332  tfr3  7058  oaabslem  7282  omabslem  7285  isinf  7723  pssnn  7728  ige2m2fzo  11836  uzindi  12047  drsdirfi  15414  ga0  16124  lbsext  17585  lindfrn  18616  fbssint  20067  filssufilg  20140  neiflim  20203  lmmbrf  21429  caucfil  21450  constr2spth  24264  constr2pth  24265  constr3lem4  24309  sspid  25300  onsucsuccmpi  29471  diophun  30298  eldioph4b  30336  dvsid  30791  dvsef  30792  cnfex  30936  dirker2re  31347  dirkerdenne0  31348  dirkerval2  31349  fourierdlem2  31364  fourierdlem3  31365  un10  32540  lhpexle1  34679
  Copyright terms: Public domain W3C validator