Theorem jctir 313

Description: Inference conjoining a theorem to right of consequent in an implication. (Contributed by NM, 31-Dec-1993.)

Hypotheses

Ref	Expression
jctil.1	|- ( ph -> ps )
jctil.2	|- ch

Assertion

Ref	Expression
jctir	|- ( ph -> ( ps /\ ch ) )

Proof of Theorem jctir

Step	Hyp	Ref	Expression
1		jctil.1	. 2 |- ( ph -> ps )
2		jctil.2	. . 3 |- ch
3	2	a1i 9	. 2 |- ( ph -> ch )
4	1, 3	jca 306	1 |- ( ph -> ( ps /\ ch ) )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  jctr  315  equvini  1781  funtp  5327  foimacnv  5540  respreima  5708  fpr  5766  dmtpos  6342  ixpsnf1o  6823  ssdomg  6870  exmidfodomrlemim  7309  archnqq  7530  recexgt0sr  7886  ige2m2fzo  10327  swrdlsw  11122  climeu  11607  algcvgblem  12371  qredeu  12419  qnumdencoprm  12515  qeqnumdivden  12516  eltg3i  14528  topbas  14539  neipsm  14626  lmbrf  14687  2lgslem1a  15565  exmidsbthrlem  15965