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  251  jcab  593  pm4.78i  772  pm3.48  775  con1dc  846  jadc  853  pm5.6r  917  exbir  1424  19.21h  1545  nford  1555  19.21ht  1569  exim  1587  i19.24  1627  equsexd  1717  equvini  1746  nfexd  1749  sbimi  1752  sbcof2  1798  nfsb2or  1825  mopick  2092  r19.32r  2612  r19.36av  2617  ceqsalt  2752  vtoclgft  2776  spcgft  2803  spcegft  2805  elab3gf  2876  mo2icl  2905  euind  2913  reu6  2915  reuind  2931  sbciegft  2981  ssddif  3356  dfiin2g  3899  invdisj  3976  ordunisuc2r  4491  fnoprabg  5943  caucvgsr  7743  rexanre  11162  tgcnp  12849  lmcvg  12857  elabgft1  13659  bj-nntrans  13833