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  3805  relcnvtr  5254  relresfld  5264  relcoi1  5266  funco  5364  foimacnv  5598  fvi  5699  isoini2  5955  ovidig  6134  smores2  6455  tfrlem5  6475  snnen2og  7040  phpm  7047  fict  7050  infnfi  7079  isinfinf  7081  exmidpw  7095  difinfinf  7294  enumct  7308  exmidfodomrlemr  7406  exmidfodomrlemrALT  7407  zsupcl  10484  infssuzex  10486  pfxccatin12lem3  11306  isumz  11943  fsumsersdc  11949  isumclim  11975  isumclim3  11977  zprodap0  12135  alzdvds  12408  bitsfzolem  12508  gcddvds  12527  dvdslegcd  12528  pclemub  12853  ennnfonelemj0  13015  ennnfonelemg  13017  ennnfonelemrn  13033  ctinf  13044  strle1g  13182  fnpr2ob  13416  metrest  15223  dvef  15444  umgrnloop2  15995  umgrclwwlkge2  16211  bj-charfunbi  16356  pw1nct  16554  nnsf  16557  exmidsbthrlem  16576