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  1769  funtp  5307  foimacnv  5518  respreima  5686  fpr  5740  dmtpos  6309  ixpsnf1o  6790  ssdomg  6832  exmidfodomrlemim  7261  archnqq  7477  recexgt0sr  7833  ige2m2fzo  10265  climeu  11439  algcvgblem  12187  qredeu  12235  qnumdencoprm  12331  qeqnumdivden  12332  eltg3i  14224  topbas  14235  neipsm  14322  lmbrf  14383  exmidsbthrlem  15512