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  5130  relresfld  5140  relcoi1  5142  funco  5238  foimacnv  5460  fvi  5553  isoini2  5798  ovidig  5970  smores2  6273  tfrlem5  6293  snnen2og  6837  phpm  6843  fict  6846  infnfi  6873  isinfinf  6875  exmidpw  6886  difinfinf  7078  enumct  7092  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  isumz  11352  fsumsersdc  11358  isumclim  11384  isumclim3  11386  zprodap0  11544  alzdvds  11814  zsupcl  11902  infssuzex  11904  gcddvds  11918  dvdslegcd  11919  pclemub  12241  ennnfonelemrn  12374  ctinf  12385  strle1g  12508  metrest  13300  dvef  13482  bj-charfunbi  13846  pw1nct  14036  nnsf  14038  exmidsbthrlem  14054