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  607  pm4.78i  789  pm3.48  792  con1dc  863  jadc  870  pm5.6r  934  exbir  1481  19.21h  1605  nford  1615  19.21ht  1629  exim  1647  i19.24  1687  equsexd  1777  equvini  1806  nfexd  1809  sbimi  1812  sbcof2  1858  nfsb2or  1885  mopick  2158  r19.32r  2679  r19.36av  2684  ceqsalt  2829  vtoclgft  2854  spcgft  2883  spcegft  2885  elab3gf  2956  mo2icl  2985  euind  2993  reu6  2995  reuind  3011  sbciegft  3062  ssddif  3441  dfiin2g  4003  invdisj  4081  ordunisuc2r  4612  fnoprabg  6121  caucvgsr  8021  rexanre  11780  tgcnp  14932  lmcvg  14940  elabgft1  16374  bj-nntrans  16546