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  5383  foimacnv  5601  respreima  5775  fpr  5836  dmtpos  6422  ixpsnf1o  6905  ssdomg  6952  exmidfodomrlemim  7412  archnqq  7637  recexgt0sr  7993  ige2m2fzo  10444  swrdlsw  11254  climeu  11874  algcvgblem  12639  qredeu  12687  qnumdencoprm  12783  qeqnumdivden  12784  eltg3i  14799  topbas  14810  neipsm  14897  lmbrf  14958  2lgslem1a  15836  usgredg2v  16094  exmidsbthrlem  16677