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  1772  funtp  5311  foimacnv  5522  respreima  5690  fpr  5744  dmtpos  6314  ixpsnf1o  6795  ssdomg  6837  exmidfodomrlemim  7268  archnqq  7484  recexgt0sr  7840  ige2m2fzo  10274  climeu  11461  algcvgblem  12217  qredeu  12265  qnumdencoprm  12361  qeqnumdivden  12362  eltg3i  14292  topbas  14303  neipsm  14390  lmbrf  14451  2lgslem1a  15329  exmidsbthrlem  15666