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  5592  respreima  5765  fpr  5825  dmtpos  6408  ixpsnf1o  6891  ssdomg  6938  exmidfodomrlemim  7390  archnqq  7615  recexgt0sr  7971  ige2m2fzo  10416  swrdlsw  11217  climeu  11823  algcvgblem  12587  qredeu  12635  qnumdencoprm  12731  qeqnumdivden  12732  eltg3i  14746  topbas  14757  neipsm  14844  lmbrf  14905  2lgslem1a  15783  usgredg2v  16038  exmidsbthrlem  16478