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  2444  brprcneu  5850  mpt2eq12  6332  tfr3  7058  oaabslem  7282  omabslem  7285  isinf  7723  pssnn  7728  ige2m2fzo  11836  uzindi  12047  drsdirfi  15414  ga0  16124  lbsext  17585  lindfrn  18616  fbssint  20067  filssufilg  20140  neiflim  20203  lmmbrf  21429  caucfil  21450  constr2spth  24264  constr2pth  24265  constr3lem4  24309  sspid  25300  onsucsuccmpi  29471  diophun  30298  eldioph4b  30336  dvsid  30791  dvsef  30792  cnfex  30936  dirker2re  31347  dirkerdenne0  31348  dirkerval2  31349  fourierdlem2  31364  fourierdlem3  31365  un10  32540  lhpexle1  34679