Theorem jctir 311

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 304	1 |- ( ph -> ( ps /\ ch ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  jctr  313  equvini  1746  funtp  5241  foimacnv  5450  respreima  5613  fpr  5667  dmtpos  6224  ixpsnf1o  6702  ssdomg  6744  exmidfodomrlemim  7157  archnqq  7358  recexgt0sr  7714  ige2m2fzo  10133  climeu  11237  algcvgblem  11981  qredeu  12029  qnumdencoprm  12125  qeqnumdivden  12126  eltg3i  12696  topbas  12707  neipsm  12794  lmbrf  12855  exmidsbthrlem  13901