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  3757  relcnvtr  5190  relresfld  5200  relcoi1  5202  funco  5299  foimacnv  5525  fvi  5621  isoini2  5869  ovidig  6044  smores2  6361  tfrlem5  6381  snnen2og  6929  phpm  6935  fict  6938  infnfi  6965  isinfinf  6967  exmidpw  6978  difinfinf  7176  enumct  7190  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  zsupcl  10338  infssuzex  10340  isumz  11571  fsumsersdc  11577  isumclim  11603  isumclim3  11605  zprodap0  11763  alzdvds  12036  bitsfzolem  12136  gcddvds  12155  dvdslegcd  12156  pclemub  12481  ennnfonelemj0  12643  ennnfonelemg  12645  ennnfonelemrn  12661  ctinf  12672  strle1g  12809  fnpr2ob  13042  metrest  14826  dvef  15047  bj-charfunbi  15541  pw1nct  15734  nnsf  15736  exmidsbthrlem  15753