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  2268  brprcneu  5518  mpt2eq12  5908  tfr3  6415  oaabslem  6641  omabslem  6644  isinf  7076  pssnn  7081  uzindi  11043  drsdirfi  14072  ga0  14752  lbsext  15916  fbssint  17533  filssufilg  17606  neiflim  17669  lmmbrf  18688  caucfil  18709  sspid  21301  ballotlem4  23057  unveldomd  23618  onsucsuccmpi  24882  dmoprabss6  25035  bsstrs  26146  diophun  26853  eldioph4b  26894  lindfrn  27291  dvsid  27548  dvsef  27549  cnfex  27699  fmuldfeq  27713  infrglb  27722  climneg  27736  stoweidlem18  27767  stoweidlem19  27768  stoweidlem22  27771  stoweidlem40  27789  stoweidlem55  27804  stirlinglem12  27834  un10  28563  lhpexle1  30197
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