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  2759  ceqsalt  2881  vtoclgft  2905  spcgft  2931  mo2icl  3015  euind  3023  reu6  3025  reuind  3039  sbciegft  3076  dfiin2g  4000  nncaddccl  4419  fnoprabg  5585