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  605  pm4.78i  787  pm3.48  790  con1dc  861  jadc  868  pm5.6r  932  exbir  1479  19.21h  1603  nford  1613  19.21ht  1627  exim  1645  i19.24  1685  equsexd  1775  equvini  1804  nfexd  1807  sbimi  1810  sbcof2  1856  nfsb2or  1883  mopick  2156  r19.32r  2677  r19.36av  2682  ceqsalt  2827  vtoclgft  2852  spcgft  2881  spcegft  2883  elab3gf  2954  mo2icl  2983  euind  2991  reu6  2993  reuind  3009  sbciegft  3060  ssddif  3439  dfiin2g  4001  invdisj  4079  ordunisuc2r  4610  fnoprabg  6117  caucvgsr  8012  rexanre  11771  tgcnp  14923  lmcvg  14931  elabgft1  16310  bj-nntrans  16482