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:  snssg  3728  relcnvtr  5150  relresfld  5160  relcoi1  5162  funco  5258  foimacnv  5481  fvi  5575  isoini2  5822  ovidig  5994  smores2  6297  tfrlem5  6317  snnen2og  6861  phpm  6867  fict  6870  infnfi  6897  isinfinf  6899  exmidpw  6910  difinfinf  7102  enumct  7116  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  isumz  11399  fsumsersdc  11405  isumclim  11431  isumclim3  11433  zprodap0  11591  alzdvds  11862  zsupcl  11950  infssuzex  11952  gcddvds  11966  dvdslegcd  11967  pclemub  12289  ennnfonelemj0  12404  ennnfonelemg  12406  ennnfonelemrn  12422  ctinf  12433  strle1g  12567  fnpr2ob  12764  metrest  14045  dvef  14227  bj-charfunbi  14602  pw1nct  14791  nnsf  14793  exmidsbthrlem  14809