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  5432  foimacnv  5655  respreima  5830  fpr  5891  dmtpos  6521  ixpsnf1o  7012  ssdomg  7059  exmidfodomrlemim  7547  archnqq  7778  recexgt0sr  8134  ige2m2fzo  10599  swrdlsw  11424  climeu  12045  algcvgblem  12810  qredeu  12858  qnumdencoprm  12954  qeqnumdivden  12955  ballotfilemfc0  13215  ballotfilemfcc  13216  eltg3i  15140  topbas  15151  neipsm  15238  lmbrf  15299  2lgslem1a  16190  usgredg2v  16448  exmidsbthrlem  17042