Theorem mpsyl 65

Description: Modus ponens combined with a syllogism inference. (Contributed by Alan Sare, 20-Apr-2011.)

Hypotheses

Ref	Expression
mpsyl.1	|- ph
mpsyl.2	|- ( ps -> ch )
mpsyl.3	|- ( ph -> ( ch -> th ) )

Assertion

Ref	Expression
mpsyl	|- ( ps -> th )

Proof of Theorem mpsyl

Step	Hyp	Ref	Expression
1		mpsyl.1	. . 3 |- ph
2	1	a1i 9	. 2 |- ( ps -> ph )
3		mpsyl.2	. 2 |- ( ps -> ch )
4		mpsyl.3	. 2 |- ( ph -> ( ch -> th ) )
5	2, 3, 4	sylc 62	1 |- ( ps -> th )

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  7081  difinfinf  7279  enumct  7293  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  zsupcl  10463  infssuzex  10465  pfxccatin12lem3  11279  isumz  11915  fsumsersdc  11921  isumclim  11947  isumclim3  11949  zprodap0  12107  alzdvds  12380  bitsfzolem  12480  gcddvds  12499  dvdslegcd  12500  pclemub  12825  ennnfonelemj0  12987  ennnfonelemg  12989  ennnfonelemrn  13005  ctinf  13016  strle1g  13154  fnpr2ob  13388  metrest  15195  dvef  15416  umgrnloop2  15964  umgrclwwlkge2  16139  bj-charfunbi  16229  pw1nct  16428  nnsf  16431  exmidsbthrlem  16450