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  3802  relcnvtr  5248  relresfld  5258  relcoi1  5260  funco  5358  foimacnv  5592  fvi  5693  isoini2  5949  ovidig  6128  smores2  6446  tfrlem5  6466  snnen2og  7028  phpm  7035  fict  7038  infnfi  7065  isinfinf  7067  exmidpw  7078  difinfinf  7276  enumct  7290  exmidfodomrlemr  7388  exmidfodomrlemrALT  7389  zsupcl  10459  infssuzex  10461  pfxccatin12lem3  11272  isumz  11908  fsumsersdc  11914  isumclim  11940  isumclim3  11942  zprodap0  12100  alzdvds  12373  bitsfzolem  12473  gcddvds  12492  dvdslegcd  12493  pclemub  12818  ennnfonelemj0  12980  ennnfonelemg  12982  ennnfonelemrn  12998  ctinf  13009  strle1g  13147  fnpr2ob  13381  metrest  15188  dvef  15409  umgrnloop2  15957  bj-charfunbi  16198  pw1nct  16398  nnsf  16401  exmidsbthrlem  16420