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  3769  relcnvtr  5207  relresfld  5217  relcoi1  5219  funco  5316  foimacnv  5547  fvi  5643  isoini2  5895  ovidig  6070  smores2  6387  tfrlem5  6407  snnen2og  6963  phpm  6969  fict  6972  infnfi  6999  isinfinf  7001  exmidpw  7012  difinfinf  7210  enumct  7224  exmidfodomrlemr  7317  exmidfodomrlemrALT  7318  zsupcl  10381  infssuzex  10383  isumz  11744  fsumsersdc  11750  isumclim  11776  isumclim3  11778  zprodap0  11936  alzdvds  12209  bitsfzolem  12309  gcddvds  12328  dvdslegcd  12329  pclemub  12654  ennnfonelemj0  12816  ennnfonelemg  12818  ennnfonelemrn  12834  ctinf  12845  strle1g  12982  fnpr2ob  13216  metrest  15022  dvef  15243  bj-charfunbi  15821  pw1nct  16014  nnsf  16016  exmidsbthrlem  16035