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

Theorem jctr 526
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 19 . 2  |-  ( ph  ->  ph )
2 jctl.1 . 2  |-  ps
31, 2jctir 524 1  |-  ( ph  ->  ( ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  mpanl2  662  mpanr2  665  bm1.1  2301  brprcneu  5556  mpt2eq12  5950  tfr3  6457  oaabslem  6683  omabslem  6686  isinf  7119  pssnn  7124  uzindi  11090  drsdirfi  14121  ga0  14801  lbsext  15965  fbssint  17585  filssufilg  17658  neiflim  17721  lmmbrf  18741  caucfil  18762  sspid  21356  unveldomd  23847  ballotlem4  23930  onsucsuccmpi  25268  diophun  26001  eldioph4b  26042  lindfrn  26439  dvsid  26696  dvsef  26697  cnfex  26847  fmuldfeq  26861  infrglb  26870  climneg  26884  stoweidlem18  26915  stoweidlem19  26916  stoweidlem22  26919  stoweidlem40  26937  stoweidlem55  26952  stirlinglem12  26982  constr2pth  27497  constr3lem4  27531  un10  28072  lhpexle1  30015
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 177  df-an 360
  Copyright terms: Public domain W3C validator