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  58  imim3i  60  imim21b  250  jcab  567  pm3.48  731  con1dc  786  jadc  793  pm4.78i  841  pm5.6r  869  exbir  1365  19.21h  1489  nford  1499  19.21ht  1513  exim  1530  i19.24  1570  equsexd  1657  equvini  1681  nfexd  1684  sbimi  1687  sbcof2  1731  nfsb2or  1758  mopick  2019  r19.32r  2501  r19.36av  2505  ceqsalt  2625  vtoclgft  2649  spcgft  2675  spcegft  2677  elab3gf  2743  mo2icl  2771  euind  2779  reu6  2781  reuind  2795  sbciegft  2844  ssddif  3198  dfiin2g  3711  invdisj  3780  ordunisuc2r  4258  fnoprabg  5622  caucvgsr  6978  rexanre  10106  elabgft1  10588  bj-nntrans  10746