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  251  jcab  592  jcn  641  pm4.78i  771  pm3.48  774  con1dc  841  jadc  848  pm5.6r  912  exbir  1412  19.21h  1536  nford  1546  19.21ht  1560  exim  1578  i19.24  1618  equsexd  1707  equvini  1731  nfexd  1734  sbimi  1737  sbcof2  1782  nfsb2or  1809  mopick  2075  r19.32r  2576  r19.36av  2580  ceqsalt  2707  vtoclgft  2731  spcgft  2758  spcegft  2760  elab3gf  2829  mo2icl  2858  euind  2866  reu6  2868  reuind  2884  sbciegft  2934  ssddif  3305  dfiin2g  3841  invdisj  3918  ordunisuc2r  4425  fnoprabg  5865  caucvgsr  7603  rexanre  10985  tgcnp  12367  lmcvg  12375  elabgft1  12974  bj-nntrans  13138