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

Theorem jctr 545
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 541 1  |-  ( ph  ->  ( ph  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  mpanl2  686  mpanr2  689  brprcneu  5856  mpt2eq12  6348  tfr3  7114  oaabslem  7341  omabslem  7344  isinf  7782  pssnn  7787  ige2m2fzo  11974  uzindi  12191  drsdirfi  16176  ga0  16945  lbsext  18379  lindfrn  19372  fbssint  20846  filssufilg  20919  neiflim  20982  lmmbrf  22225  caucfil  22246  constr2spth  25323  constr2pth  25324  constr3lem4  25368  efghgrpOLD  26094  sspid  26357  onsucsuccmpi  31096  poimirlem28  31961  lhpexle1  33567  diophun  35610  eldioph4b  35648  relexp1idm  36300  relexp0idm  36301  dvsid  36674  dvsef  36675  un10  37169  cnfex  37343  dvmptfprod  37814
  Copyright terms: Public domain W3C validator