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  1781  funtp  5328  foimacnv  5542  respreima  5710  fpr  5768  dmtpos  6344  ixpsnf1o  6825  ssdomg  6872  exmidfodomrlemim  7311  archnqq  7532  recexgt0sr  7888  ige2m2fzo  10329  swrdlsw  11125  climeu  11640  algcvgblem  12404  qredeu  12452  qnumdencoprm  12548  qeqnumdivden  12549  eltg3i  14561  topbas  14572  neipsm  14659  lmbrf  14720  2lgslem1a  15598  exmidsbthrlem  15998