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  1751  funtp  5251  foimacnv  5460  respreima  5624  fpr  5678  dmtpos  6235  ixpsnf1o  6714  ssdomg  6756  exmidfodomrlemim  7178  archnqq  7379  recexgt0sr  7735  ige2m2fzo  10154  climeu  11259  algcvgblem  12003  qredeu  12051  qnumdencoprm  12147  qeqnumdivden  12148  eltg3i  12850  topbas  12861  neipsm  12948  lmbrf  13009  exmidsbthrlem  14054