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  5312  foimacnv  5525  respreima  5693  fpr  5747  dmtpos  6323  ixpsnf1o  6804  ssdomg  6846  exmidfodomrlemim  7280  archnqq  7501  recexgt0sr  7857  ige2m2fzo  10291  climeu  11478  algcvgblem  12242  qredeu  12290  qnumdencoprm  12386  qeqnumdivden  12387  eltg3i  14376  topbas  14387  neipsm  14474  lmbrf  14535  2lgslem1a  15413  exmidsbthrlem  15753