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  10491  infssuzex  10493  pfxccatin12lem3  11313  isumz  11951  fsumsersdc  11957  isumclim  11983  isumclim3  11985  zprodap0  12143  alzdvds  12416  bitsfzolem  12516  gcddvds  12535  dvdslegcd  12536  pclemub  12861  ennnfonelemj0  13023  ennnfonelemg  13025  ennnfonelemrn  13041  ctinf  13052  strle1g  13190  fnpr2ob  13424  metrest  15232  dvef  15453  umgrnloop2  16004  umgrclwwlkge2  16255  bj-charfunbi  16409  pw1nct  16607  nnsf  16610  exmidsbthrlem  16629