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  3726  relcnvtr  5148  relresfld  5158  relcoi1  5160  funco  5256  foimacnv  5479  fvi  5573  isoini2  5819  ovidig  5991  smores2  6294  tfrlem5  6314  snnen2og  6858  phpm  6864  fict  6867  infnfi  6894  isinfinf  6896  exmidpw  6907  difinfinf  7099  enumct  7113  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  isumz  11396  fsumsersdc  11402  isumclim  11428  isumclim3  11430  zprodap0  11588  alzdvds  11859  zsupcl  11947  infssuzex  11949  gcddvds  11963  dvdslegcd  11964  pclemub  12286  ennnfonelemj0  12401  ennnfonelemg  12403  ennnfonelemrn  12419  ctinf  12430  strle1g  12564  fnpr2ob  12758  metrest  13976  dvef  14158  bj-charfunbi  14533  pw1nct  14722  nnsf  14724  exmidsbthrlem  14740