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  782  pm3.48  785  con1dc  856  jadc  863  pm5.6r  927  exbir  1436  19.21h  1557  nford  1567  19.21ht  1581  exim  1599  i19.24  1639  equsexd  1729  equvini  1758  nfexd  1761  sbimi  1764  sbcof2  1810  nfsb2or  1837  mopick  2104  r19.32r  2623  r19.36av  2628  ceqsalt  2765  vtoclgft  2789  spcgft  2816  spcegft  2818  elab3gf  2889  mo2icl  2918  euind  2926  reu6  2928  reuind  2944  sbciegft  2995  ssddif  3371  dfiin2g  3921  invdisj  3999  ordunisuc2r  4515  fnoprabg  5978  caucvgsr  7803  rexanre  11231  tgcnp  13748  lmcvg  13756  elabgft1  14569  bj-nntrans  14742