Theorem mpsyl 59

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

Hypotheses

Ref	Expression
mpsyl.1	⊢ φ
mpsyl.2	⊢ (ψ → χ)
mpsyl.3	⊢ (φ → (χ → θ))

Assertion

Ref	Expression
mpsyl	⊢ (ψ → θ)

Proof of Theorem mpsyl

Step	Hyp	Ref	Expression
1		mpsyl.1	. . 3 ⊢ φ
2	1	a1i 10	. 2 ⊢ (ψ → φ)
3		mpsyl.2	. 2 ⊢ (ψ → χ)
4		mpsyl.3	. 2 ⊢ (φ → (χ → θ))
5	2, 3, 4	sylc 56	1 ⊢ (ψ → θ)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

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