Theorem jctr 540

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

Syntax hints:   -> wi 4   /\ wa 367

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 369

This theorem is referenced by:  mpanl2  679  mpanr2  682  bm1.1OLD  2386  brprcneu  5842  mpt2eq12  6338  tfr3  7102  oaabslem  7329  omabslem  7332  isinf  7768  pssnn  7773  ige2m2fzo  11915  uzindi  12132  drsdirfi  15891  ga0  16660  lbsext  18129  lindfrn  19148  fbssint  20631  filssufilg  20704  neiflim  20767  lmmbrf  21993  caucfil  22014  constr2spth  25019  constr2pth  25020  constr3lem4  25064  efghgrpOLD  25789  sspid  26052  onsucsuccmpi  30675  lhpexle1  33025  diophun  35068  eldioph4b  35106  relexp1idm  35693  relexp0idm  35694  dvsid  36084  dvsef  36085  un10  36609  cnfex  36783  dvmptfprod  37110