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 ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  imim12i  59  imim3i  61  imim21b  253  jcab  603  pm4.78i  783  pm3.48  786  con1dc  857  jadc  864  pm5.6r  928  exbir  1447  19.21h  1568  nford  1578  19.21ht  1592  exim  1610  i19.24  1650  equsexd  1740  equvini  1769  nfexd  1772  sbimi  1775  sbcof2  1821  nfsb2or  1848  mopick  2116  r19.32r  2636  r19.36av  2641  ceqsalt  2778  vtoclgft  2802  spcgft  2829  spcegft  2831  elab3gf  2902  mo2icl  2931  euind  2939  reu6  2941  reuind  2957  sbciegft  3008  ssddif  3384  dfiin2g  3934  invdisj  4012  ordunisuc2r  4531  fnoprabg  5997  caucvgsr  7831  rexanre  11261  tgcnp  14169  lmcvg  14177  elabgft1  14991  bj-nntrans  15164