Theorem imim2i 13

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 10	. 2 |- (ch -> (ph -> ps))
3	2	a2i 12	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  53  imim3i  55  ja  153  imim21b  356  pm3.48  806  jcab  833  exbir  1365  nic-ax  1438  nic-axALT  1439  tbw-bijust  1463  merco1  1478  sbimi  1652  19.24  1662  nfimdOLD  1809  19.21hOLD  1840  19.21tOLD  1863  ax12olem3  1929  ax11indi  2196  mopick  2266  axi5r  2326  r19.36av  2760  ceqsalt  2882  vtoclgft  2906  spcgft  2932  mo2icl  3016  euind  3024  reu6  3026  reuind  3040  sbciegft  3077  dfiin2g  4001  nncaddccl  4420  fnoprabg  5586