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  1456  19.21h  1580  nford  1590  19.21ht  1604  exim  1622  i19.24  1662  equsexd  1752  equvini  1781  nfexd  1784  sbimi  1787  sbcof2  1833  nfsb2or  1860  mopick  2132  r19.32r  2652  r19.36av  2657  ceqsalt  2798  vtoclgft  2823  spcgft  2850  spcegft  2852  elab3gf  2923  mo2icl  2952  euind  2960  reu6  2962  reuind  2978  sbciegft  3029  ssddif  3407  dfiin2g  3960  invdisj  4038  ordunisuc2r  4562  fnoprabg  6046  caucvgsr  7915  rexanre  11531  tgcnp  14681  lmcvg  14689  elabgft1  15714  bj-nntrans  15887