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  1758  funtp  5271  foimacnv  5481  respreima  5646  fpr  5700  dmtpos  6259  ixpsnf1o  6738  ssdomg  6780  exmidfodomrlemim  7202  archnqq  7418  recexgt0sr  7774  ige2m2fzo  10200  climeu  11306  algcvgblem  12051  qredeu  12099  qnumdencoprm  12195  qeqnumdivden  12196  eltg3i  13641  topbas  13652  neipsm  13739  lmbrf  13800  exmidsbthrlem  14855