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  5251  relresfld  5261  relcoi1  5263  funco  5361  foimacnv  5595  fvi  5696  isoini2  5952  ovidig  6131  smores2  6451  tfrlem5  6471  snnen2og  7033  phpm  7040  fict  7043  infnfi  7070  isinfinf  7072  exmidpw  7086  difinfinf  7284  enumct  7298  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  zsupcl  10468  infssuzex  10470  pfxccatin12lem3  11285  isumz  11921  fsumsersdc  11927  isumclim  11953  isumclim3  11955  zprodap0  12113  alzdvds  12386  bitsfzolem  12486  gcddvds  12505  dvdslegcd  12506  pclemub  12831  ennnfonelemj0  12993  ennnfonelemg  12995  ennnfonelemrn  13011  ctinf  13022  strle1g  13160  fnpr2ob  13394  metrest  15201  dvef  15422  umgrnloop2  15970  umgrclwwlkge2  16171  bj-charfunbi  16283  pw1nct  16482  nnsf  16485  exmidsbthrlem  16504