Theorem mpsyl 65

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 62	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:  relcnvtr  5058  relresfld  5068  relcoi1  5070  funco  5163  foimacnv  5385  fvi  5478  isoini2  5720  ovidig  5888  smores2  6191  tfrlem5  6211  snnen2og  6753  phpm  6759  fict  6762  infnfi  6789  isinfinf  6791  exmidpw  6802  difinfinf  6986  enumct  7000  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  isumz  11158  fsumsersdc  11164  isumclim  11190  isumclim3  11192  alzdvds  11552  zsupcl  11640  infssuzex  11642  gcddvds  11652  dvdslegcd  11653  ennnfonelemrn  11932  ctinf  11943  strle1g  12049  metrest  12675  dvef  12856  nnsf  13199  exmidsbthrlem  13217