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  10616  swrdlsw  11441  climeu  12062  algcvgblem  12827  qredeu  12875  qnumdencoprm  12971  qeqnumdivden  12972  ballotfilemfc0  13232  ballotfilemfcc  13233  eltg3i  15157  topbas  15168  neipsm  15255  lmbrf  15316  2lgslem1a  16207  usgredg2v  16465  exmidsbthrlem  17067