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  4783  relresfld  4790  relcoi1  4792  funco  4883  foimacnv  5087  fvi  5173  isoini2  5401  ovidig  5560  smores2  5850  tfrlem5  5871  cauappcvgprlemm  6617  caucvgprlemm  6639