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  1807  funtp  5414  foimacnv  5637  respreima  5810  fpr  5871  dmtpos  6500  ixpsnf1o  6984  ssdomg  7031  exmidfodomrlemim  7517  archnqq  7748  recexgt0sr  8104  ige2m2fzo  10565  swrdlsw  11386  climeu  12006  algcvgblem  12771  qredeu  12819  qnumdencoprm  12915  qeqnumdivden  12916  ballotfilemfc0  13176  ballotfilemfcc  13177  eltg3i  15047  topbas  15058  neipsm  15145  lmbrf  15206  2lgslem1a  16087  usgredg2v  16345  exmidsbthrlem  16928