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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  jctr  315  equvini  1811  funtp  5434  foimacnv  5657  respreima  5836  fpr  5897  dmtpos  6527  ixpsnf1o  7018  ssdomg  7065  exmidfodomrlemim  7553  archnqq  7784  recexgt0sr  8140  ige2m2fzo  10626  swrdlsw  11455  climeu  12078  algcvgblem  12843  qredeu  12891  qnumdencoprm  12989  qeqnumdivden  12990  ballotfilemfc0  13281  ballotfilemfcc  13282  eltg3i  15206  topbas  15217  neipsm  15304  lmbrf  15365  bcmono  16202  2lgslem1a  16305  usgredg2v  16563  exmidsbthrlem  17165