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	|- ps

Assertion

Ref	Expression
jctr	|- ( ph -> ( ph /\ ps ) )

Proof of Theorem jctr

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( ph -> ph )
2		jctl.1	. 2 |- ps
3	1, 2	jctir 538	1 |- ( ph -> ( ph /\ ps ) )

Syntax hints:   -> wi 4   /\ wa 369

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

This theorem is referenced by:  mpanl2  681  mpanr2  684  bm1.1OLD  2428  brprcneu  5703  mpt2eq12  6165  tfr3  6877  oaabslem  7101  omabslem  7104  isinf  7545  pssnn  7550  uzindi  11822  drsdirfi  15127  ga0  15835  lbsext  17263  lindfrn  18269  fbssint  19430  filssufilg  19503  neiflim  19566  lmmbrf  20792  caucfil  20813  constr2spth  23518  constr2pth  23519  constr3lem4  23552  sspid  24142  onsucsuccmpi  28308  diophun  29135  eldioph4b  29173  dvsid  29628  dvsef  29629  cnfex  29773  ige2m2fzo  30243  un10  31544  lhpexle1  33675