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

Step	Hyp	Ref	Expression
1		id 22	. 2
2		jctl.1	. 2
3	1, 2	jctir 538	1

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