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  3807  relcnvtr  5256  relresfld  5266  relcoi1  5268  funco  5366  foimacnv  5601  fvi  5703  isoini2  5960  ovidig  6139  smores2  6460  tfrlem5  6480  snnen2og  7045  phpm  7052  fict  7055  infnfi  7084  isinfinf  7086  exmidpw  7100  difinfinf  7300  enumct  7314  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  zsupcl  10492  infssuzex  10494  pfxccatin12lem3  11314  isumz  11952  fsumsersdc  11958  isumclim  11984  isumclim3  11986  zprodap0  12144  alzdvds  12417  bitsfzolem  12517  gcddvds  12536  dvdslegcd  12537  pclemub  12862  ennnfonelemj0  13024  ennnfonelemg  13026  ennnfonelemrn  13042  ctinf  13053  strle1g  13191  fnpr2ob  13425  metrest  15233  dvef  15454  umgrnloop2  16005  umgrclwwlkge2  16256  bj-charfunbi  16427  pw1nct  16625  nnsf  16628  exmidsbthrlem  16647