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  611  pm4.78i  794  pm3.48  797  con1dc  868  jadc  875  pm5.6r  939  exbir  1486  19.21h  1610  nford  1620  19.21ht  1634  exim  1652  i19.24  1692  equsexd  1782  equvini  1811  nfexd  1814  sbimi  1817  sbcof2  1863  nfsb2or  1890  mopick  2165  r19.32r  2697  r19.36av  2702  ceqsalt  2848  vtoclgft  2873  spcgft  2902  spcegft  2904  elab3gf  2976  mo2icl  3005  euind  3013  reu6  3015  reuind  3031  sbciegft  3082  ssddif  3465  dfiin2g  4040  invdisj  4118  ordunisuc2r  4656  fnoprabg  6179  caucvgsr  8159  rexanre  11964  tgcnp  15233  lmcvg  15241  elabgft1  16720  bj-nntrans  16891