Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  jctr 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
Assertion
Ref Expression
jctr

Proof of Theorem jctr
StepHypRef Expression
1 id 22 . 2
2 jctl.1 . 2
31, 2jctir 538 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369 This theorem is referenced by:  mpanl2  681  mpanr2  684  bm1.1OLD  2441  brprcneu  5864  mpt2eq12  6357  tfr3  7087  oaabslem  7311  omabslem  7314  isinf  7753  pssnn  7758  ige2m2fzo  11879  uzindi  12091  drsdirfi  15567  ga0  16336  lbsext  17809  lindfrn  18856  fbssint  20339  filssufilg  20412  neiflim  20475  lmmbrf  21701  caucfil  21722  constr2spth  24602  constr2pth  24603  constr3lem4  24647  efghgrpOLD  25375  sspid  25638  onsucsuccmpi  29908  diophun  30707  eldioph4b  30745  dvsid  31236  dvsef  31237  cnfex  31403  dvmptfprod  31742  un10  33585  lhpexle1  35732 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
 Copyright terms: Public domain W3C validator