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  59  imim3i  61  imim21b  251  jcab  571  pm3.48  735  con1dc  792  jadc  799  pm4.78i  847  pm5.6r  875  exbir  1371  19.21h  1495  nford  1505  19.21ht  1519  exim  1536  i19.24  1576  equsexd  1665  equvini  1689  nfexd  1692  sbimi  1695  sbcof2  1739  nfsb2or  1766  mopick  2027  r19.32r  2517  r19.36av  2521  ceqsalt  2648  vtoclgft  2672  spcgft  2699  spcegft  2701  elab3gf  2768  mo2icl  2797  euind  2805  reu6  2807  reuind  2823  sbciegft  2872  ssddif  3236  dfiin2g  3771  invdisj  3847  ordunisuc2r  4346  fnoprabg  5762  caucvgsr  7410  rexanre  10716  elabgft1  11982  bj-nntrans  12150