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  3767  relcnvtr  5202  relresfld  5212  relcoi1  5214  funco  5311  foimacnv  5540  fvi  5636  isoini2  5888  ovidig  6063  smores2  6380  tfrlem5  6400  snnen2og  6956  phpm  6962  fict  6965  infnfi  6992  isinfinf  6994  exmidpw  7005  difinfinf  7203  enumct  7217  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  zsupcl  10374  infssuzex  10376  isumz  11700  fsumsersdc  11706  isumclim  11732  isumclim3  11734  zprodap0  11892  alzdvds  12165  bitsfzolem  12265  gcddvds  12284  dvdslegcd  12285  pclemub  12610  ennnfonelemj0  12772  ennnfonelemg  12774  ennnfonelemrn  12790  ctinf  12801  strle1g  12938  fnpr2ob  13172  metrest  14978  dvef  15199  bj-charfunbi  15747  pw1nct  15940  nnsf  15942  exmidsbthrlem  15961