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  783  pm3.48  786  con1dc  857  jadc  864  pm5.6r  928  exbir  1447  19.21h  1568  nford  1578  19.21ht  1592  exim  1610  i19.24  1650  equsexd  1740  equvini  1769  nfexd  1772  sbimi  1775  sbcof2  1821  nfsb2or  1848  mopick  2120  r19.32r  2640  r19.36av  2645  ceqsalt  2786  vtoclgft  2810  spcgft  2837  spcegft  2839  elab3gf  2910  mo2icl  2939  euind  2947  reu6  2949  reuind  2965  sbciegft  3016  ssddif  3393  dfiin2g  3945  invdisj  4023  ordunisuc2r  4546  fnoprabg  6019  caucvgsr  7862  rexanre  11364  tgcnp  14377  lmcvg  14385  elabgft1  15270  bj-nntrans  15443