Theorem imim2i 12

Description: Inference adding common antecedents in an implication. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
imim2i.1	|- ( ph -> ps )

Assertion

Ref	Expression
imim2i	|- ( ( ch -> ph ) -> ( ch -> ps ) )

Proof of Theorem imim2i

Step	Hyp	Ref	Expression
1		imim2i.1	. . 3 |- ( ph -> ps )
2	1	a1i 9	. 2 |- ( ch -> ( ph -> ps ) )
3	2	a2i 11	1 |- ( ( ch -> ph ) -> ( ch -> ps ) )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  imim12i  59  imim3i  61  imim21b  253  jcab  611  pm4.78i  794  pm3.48  797  con1dc  868  jadc  875  pm5.6r  939  exbir  1486  19.21h  1610  nford  1620  19.21ht  1634  exim  1652  i19.24  1692  equsexd  1782  equvini  1811  nfexd  1814  sbimi  1817  sbcof2  1863  nfsb2or  1890  mopick  2165  r19.32r  2697  r19.36av  2702  ceqsalt  2848  vtoclgft  2873  spcgft  2902  spcegft  2904  elab3gf  2976  mo2icl  3005  euind  3013  reu6  3015  reuind  3031  sbciegft  3082  ssddif  3465  dfiin2g  4045  invdisj  4123  ordunisuc2r  4661  fnoprabg  6189  caucvgsr  8169  rexanre  11986  tgcnp  15310  lmcvg  15318  elabgft1  16806  bj-nntrans  16977