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  1571  nford  1581  19.21ht  1595  exim  1613  i19.24  1653  equsexd  1743  equvini  1772  nfexd  1775  sbimi  1778  sbcof2  1824  nfsb2or  1851  mopick  2123  r19.32r  2643  r19.36av  2648  ceqsalt  2789  vtoclgft  2814  spcgft  2841  spcegft  2843  elab3gf  2914  mo2icl  2943  euind  2951  reu6  2953  reuind  2969  sbciegft  3020  ssddif  3398  dfiin2g  3950  invdisj  4028  ordunisuc2r  4551  fnoprabg  6027  caucvgsr  7886  rexanre  11402  tgcnp  14529  lmcvg  14537  elabgft1  15508  bj-nntrans  15681