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  1806  funtp  5390  foimacnv  5610  respreima  5783  fpr  5844  dmtpos  6465  ixpsnf1o  6948  ssdomg  6995  exmidfodomrlemim  7472  archnqq  7697  recexgt0sr  8053  ige2m2fzo  10506  swrdlsw  11316  climeu  11936  algcvgblem  12701  qredeu  12749  qnumdencoprm  12845  qeqnumdivden  12846  eltg3i  14867  topbas  14878  neipsm  14965  lmbrf  15026  2lgslem1a  15907  usgredg2v  16165  exmidsbthrlem  16750