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  3738  relcnvtr  5160  relresfld  5170  relcoi1  5172  funco  5268  foimacnv  5491  fvi  5586  isoini2  5833  ovidig  6006  smores2  6309  tfrlem5  6329  snnen2og  6873  phpm  6879  fict  6882  infnfi  6909  isinfinf  6911  exmidpw  6922  difinfinf  7114  enumct  7128  exmidfodomrlemr  7215  exmidfodomrlemrALT  7216  isumz  11411  fsumsersdc  11417  isumclim  11443  isumclim3  11445  zprodap0  11603  alzdvds  11874  zsupcl  11962  infssuzex  11964  gcddvds  11978  dvdslegcd  11979  pclemub  12301  ennnfonelemj0  12416  ennnfonelemg  12418  ennnfonelemrn  12434  ctinf  12445  strle1g  12580  fnpr2ob  12778  metrest  14359  dvef  14541  bj-charfunbi  14916  pw1nct  15106  nnsf  15108  exmidsbthrlem  15124