Theorem mpsyl 59

Description: Modus ponens combined with a syllogism inference. (Contributed by Alan Sare, 20-Apr-2011.)

Hypotheses

Ref	Expression
mpsyl.1	|- ph
mpsyl.2	|- (ps -> ch)
mpsyl.3	|- (ph -> (ch -> th))

Assertion

Ref	Expression
mpsyl	|- (ps -> th)

Proof of Theorem mpsyl

Step	Hyp	Ref	Expression
1		mpsyl.1	. . 3 |- ph
2	1	a1i 10	. 2 |- (ps -> ph)
3		mpsyl.2	. 2 |- (ps -> ch)
4		mpsyl.3	. 2 |- (ph -> (ch -> th))
5	2, 3, 4	sylc 56	1 |- (ps -> th)

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  tbwlem1  1470  tbwlem2  1471  re1luk3  1477  merco1lem17  1498  re1tbw1  1510  a16g  1945  funmo  5126  foimacnv  5304  isoini2  5499