Theorem mpsyl 64

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 61	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  4860  relresfld  4867  relcoi1  4869  funco  4960  foimacnv  5164  fvi  5251  isoini2  5478  ovidig  5638  smores2  5932  tfrlem5  5953  snnen2og  6345  phpm  6351  cauappcvgprlemm  6835  caucvgprlemm  6858  caucvgprprlemml  6884  caucvgsr  6978  alzdvds  10254  zsupcl  10343  infssuzex  10345  gcddvds  10355  dvdslegcd  10356