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:  relcnvtr  5053  relresfld  5063  relcoi1  5065  funco  5158  foimacnv  5378  fvi  5471  isoini2  5713  ovidig  5881  smores2  6184  tfrlem5  6204  snnen2og  6746  phpm  6752  fict  6755  infnfi  6782  isinfinf  6784  exmidpw  6795  difinfinf  6979  enumct  6993  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  isumz  11151  fsumsersdc  11157  isumclim  11183  isumclim3  11185  alzdvds  11541  zsupcl  11629  infssuzex  11631  gcddvds  11641  dvdslegcd  11642  ennnfonelemrn  11921  ctinf  11932  strle1g  12038  metrest  12664  dvef  12845  nnsf  13188  exmidsbthrlem  13206