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  3781  relcnvtr  5224  relresfld  5234  relcoi1  5236  funco  5334  foimacnv  5566  fvi  5664  isoini2  5916  ovidig  6093  smores2  6410  tfrlem5  6430  snnen2og  6988  phpm  6995  fict  6998  infnfi  7025  isinfinf  7027  exmidpw  7038  difinfinf  7236  enumct  7250  exmidfodomrlemr  7348  exmidfodomrlemrALT  7349  zsupcl  10418  infssuzex  10420  pfxccatin12lem3  11230  isumz  11866  fsumsersdc  11872  isumclim  11898  isumclim3  11900  zprodap0  12058  alzdvds  12331  bitsfzolem  12431  gcddvds  12450  dvdslegcd  12451  pclemub  12776  ennnfonelemj0  12938  ennnfonelemg  12940  ennnfonelemrn  12956  ctinf  12967  strle1g  13105  fnpr2ob  13339  metrest  15145  dvef  15366  umgrnloop2  15914  bj-charfunbi  16084  pw1nct  16280  nnsf  16282  exmidsbthrlem  16301