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  3808  relcnvtr  5258  relresfld  5268  relcoi1  5270  funco  5368  foimacnv  5604  fvi  5706  isoini2  5965  ovidig  6144  smores2  6465  tfrlem5  6485  snnen2og  7050  phpm  7057  fict  7060  infnfi  7089  isinfinf  7091  exmidpw  7105  difinfinf  7305  enumct  7319  exmidfodomrlemr  7418  exmidfodomrlemrALT  7419  zsupcl  10497  infssuzex  10499  pfxccatin12lem3  11322  isumz  11973  fsumsersdc  11979  isumclim  12005  isumclim3  12007  zprodap0  12165  alzdvds  12438  bitsfzolem  12538  gcddvds  12557  dvdslegcd  12558  pclemub  12883  ennnfonelemj0  13045  ennnfonelemg  13047  ennnfonelemrn  13063  ctinf  13074  strle1g  13212  fnpr2ob  13446  metrest  15259  dvef  15480  umgrnloop2  16031  umgrclwwlkge2  16282  bj-charfunbi  16466  pw1nct  16664  nnsf  16670  exmidsbthrlem  16689