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  1731  funtp  5176  foimacnv  5385  respreima  5548  fpr  5602  dmtpos  6153  ixpsnf1o  6630  ssdomg  6672  exmidfodomrlemim  7057  archnqq  7225  recexgt0sr  7581  ige2m2fzo  9975  climeu  11065  algcvgblem  11730  qredeu  11778  qnumdencoprm  11871  qeqnumdivden  11872  eltg3i  12225  topbas  12236  neipsm  12323  lmbrf  12384  exmidsbthrlem  13217