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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  imim12i  58  imim3i  60  imim21b  250  jcab  570  pm3.48  734  con1dc  791  jadc  798  pm4.78i  846  pm5.6r  874  exbir  1370  19.21h  1494  nford  1504  19.21ht  1518  exim  1535  i19.24  1575  equsexd  1664  equvini  1688  nfexd  1691  sbimi  1694  sbcof2  1738  nfsb2or  1765  mopick  2026  r19.32r  2514  r19.36av  2518  ceqsalt  2645  vtoclgft  2669  spcgft  2696  spcegft  2698  elab3gf  2763  mo2icl  2792  euind  2800  reu6  2802  reuind  2818  sbciegft  2867  ssddif  3231  dfiin2g  3758  invdisj  3831  ordunisuc2r  4321  fnoprabg  5728  caucvgsr  7326  rexanre  10618  elabgft1  11335  bj-nntrans  11503