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

Theorem jctr 540
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 536 1  |-  ( ph  ->  ( ph  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  mpanl2  679  mpanr2  682  bm1.1OLD  2386  brprcneu  5842  mpt2eq12  6338  tfr3  7102  oaabslem  7329  omabslem  7332  isinf  7768  pssnn  7773  ige2m2fzo  11915  uzindi  12132  drsdirfi  15891  ga0  16660  lbsext  18129  lindfrn  19148  fbssint  20631  filssufilg  20704  neiflim  20767  lmmbrf  21993  caucfil  22014  constr2spth  25019  constr2pth  25020  constr3lem4  25064  efghgrpOLD  25789  sspid  26052  onsucsuccmpi  30675  lhpexle1  33025  diophun  35068  eldioph4b  35106  relexp1idm  35693  relexp0idm  35694  dvsid  36084  dvsef  36085  un10  36609  cnfex  36783  dvmptfprod  37110
  Copyright terms: Public domain W3C validator