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 9	. 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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  relcnvtr  4763  relresfld  4770  relcoi1  4772  funco  4862  foimacnv  5065  fvi  5151  isoini2  5379  ovidig  5537  smores2  5827  tfrlem5  5848