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  1804  funtp  5374  foimacnv  5590  respreima  5763  fpr  5821  dmtpos  6402  ixpsnf1o  6883  ssdomg  6930  exmidfodomrlemim  7379  archnqq  7604  recexgt0sr  7960  ige2m2fzo  10404  swrdlsw  11201  climeu  11807  algcvgblem  12571  qredeu  12619  qnumdencoprm  12715  qeqnumdivden  12716  eltg3i  14730  topbas  14741  neipsm  14828  lmbrf  14889  2lgslem1a  15767  usgredg2v  16022  exmidsbthrlem  16390