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  5122  relresfld  5132  relcoi1  5134  funco  5227  foimacnv  5449  fvi  5542  isoini2  5786  ovidig  5955  smores2  6258  tfrlem5  6278  snnen2og  6821  phpm  6827  fict  6830  infnfi  6857  isinfinf  6859  exmidpw  6870  difinfinf  7062  enumct  7076  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  isumz  11326  fsumsersdc  11332  isumclim  11358  isumclim3  11360  zprodap0  11518  alzdvds  11788  zsupcl  11876  infssuzex  11878  gcddvds  11892  dvdslegcd  11893  pclemub  12215  ennnfonelemrn  12348  ctinf  12359  strle1g  12480  metrest  13106  dvef  13288  bj-charfunbi  13653  pw1nct  13843  nnsf  13845  exmidsbthrlem  13861