Theorem jctr 545

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 541	1 |- ( ph -> ( ph /\ ps ) )

Syntax hints:   -> wi 4   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  mpanl2  686  mpanr2  689  brprcneu  5856  mpt2eq12  6348  tfr3  7114  oaabslem  7341  omabslem  7344  isinf  7782  pssnn  7787  ige2m2fzo  11974  uzindi  12191  drsdirfi  16176  ga0  16945  lbsext  18379  lindfrn  19372  fbssint  20846  filssufilg  20919  neiflim  20982  lmmbrf  22225  caucfil  22246  constr2spth  25323  constr2pth  25324  constr3lem4  25368  efghgrpOLD  26094  sspid  26357  onsucsuccmpi  31096  poimirlem28  31961  lhpexle1  33567  diophun  35610  eldioph4b  35648  relexp1idm  36300  relexp0idm  36301  dvsid  36674  dvsef  36675  un10  37169  cnfex  37343  dvmptfprod  37814