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  784  pm3.48  787  con1dc  858  jadc  865  pm5.6r  929  exbir  1457  19.21h  1581  nford  1591  19.21ht  1605  exim  1623  i19.24  1663  equsexd  1753  equvini  1782  nfexd  1785  sbimi  1788  sbcof2  1834  nfsb2or  1861  mopick  2134  r19.32r  2654  r19.36av  2659  ceqsalt  2803  vtoclgft  2828  spcgft  2857  spcegft  2859  elab3gf  2930  mo2icl  2959  euind  2967  reu6  2969  reuind  2985  sbciegft  3036  ssddif  3415  dfiin2g  3974  invdisj  4052  ordunisuc2r  4580  fnoprabg  6069  caucvgsr  7950  rexanre  11646  tgcnp  14796  lmcvg  14804  elabgft1  15914  bj-nntrans  16086