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  607  pm4.78i  790  pm3.48  793  con1dc  864  jadc  871  pm5.6r  935  exbir  1482  19.21h  1606  nford  1616  19.21ht  1630  exim  1648  i19.24  1688  equsexd  1778  equvini  1807  nfexd  1810  sbimi  1813  sbcof2  1859  nfsb2or  1886  mopick  2159  r19.32r  2689  r19.36av  2694  ceqsalt  2840  vtoclgft  2865  spcgft  2894  spcegft  2896  elab3gf  2967  mo2icl  2996  euind  3004  reu6  3006  reuind  3022  sbciegft  3073  ssddif  3455  dfiin2g  4024  invdisj  4102  ordunisuc2r  4636  fnoprabg  6154  caucvgsr  8117  rexanre  11905  tgcnp  15074  lmcvg  15082  elabgft1  16550  bj-nntrans  16721