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  3757  relcnvtr  5190  relresfld  5200  relcoi1  5202  funco  5299  foimacnv  5525  fvi  5621  isoini2  5869  ovidig  6044  smores2  6361  tfrlem5  6381  snnen2og  6929  phpm  6935  fict  6938  infnfi  6965  isinfinf  6967  exmidpw  6978  difinfinf  7176  enumct  7190  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  zsupcl  10340  infssuzex  10342  isumz  11573  fsumsersdc  11579  isumclim  11605  isumclim3  11607  zprodap0  11765  alzdvds  12038  bitsfzolem  12138  gcddvds  12157  dvdslegcd  12158  pclemub  12483  ennnfonelemj0  12645  ennnfonelemg  12647  ennnfonelemrn  12663  ctinf  12674  strle1g  12811  fnpr2ob  13044  metrest  14850  dvef  15071  bj-charfunbi  15565  pw1nct  15758  nnsf  15760  exmidsbthrlem  15779