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  53  imim3i  55  imim21b  241  jcab  535  pm3.48  699  con1dc  753  jadc  760  pm4.78i  808  pm5.6r  836  exbir  1325  19.21h  1449  nford  1459  19.21ht  1473  exim  1490  i19.24  1530  equsexd  1617  equvini  1641  nfexd  1644  sbimi  1647  sbcof2  1691  nfsb2or  1718  mopick  1978  r19.32r  2457  r19.36av  2461  ceqsalt  2580  vtoclgft  2604  spcgft  2630  spcegft  2632  elab3gf  2692  mo2icl  2720  euind  2728  reu6  2730  reuind  2744  sbciegft  2793  ssddif  3171  dfiin2g  3690  invdisj  3759  ordunisuc2r  4240  fnoprabg  5602  caucvgsr  6886  elabgft1  9917  bj-nntrans  10076