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  1782  funtp  5346  foimacnv  5562  respreima  5731  fpr  5789  dmtpos  6365  ixpsnf1o  6846  ssdomg  6893  exmidfodomrlemim  7340  archnqq  7565  recexgt0sr  7921  ige2m2fzo  10364  swrdlsw  11160  climeu  11722  algcvgblem  12486  qredeu  12534  qnumdencoprm  12630  qeqnumdivden  12631  eltg3i  14643  topbas  14654  neipsm  14741  lmbrf  14802  2lgslem1a  15680  exmidsbthrlem  16163