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  3801  relcnvtr  5247  relresfld  5257  relcoi1  5259  funco  5357  foimacnv  5589  fvi  5690  isoini2  5942  ovidig  6121  smores2  6438  tfrlem5  6458  snnen2og  7016  phpm  7023  fict  7026  infnfi  7053  isinfinf  7055  exmidpw  7066  difinfinf  7264  enumct  7278  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  zsupcl  10446  infssuzex  10448  pfxccatin12lem3  11259  isumz  11895  fsumsersdc  11901  isumclim  11927  isumclim3  11929  zprodap0  12087  alzdvds  12360  bitsfzolem  12460  gcddvds  12479  dvdslegcd  12480  pclemub  12805  ennnfonelemj0  12967  ennnfonelemg  12969  ennnfonelemrn  12985  ctinf  12996  strle1g  13134  fnpr2ob  13368  metrest  15174  dvef  15395  umgrnloop2  15943  bj-charfunbi  16132  pw1nct  16328  nnsf  16330  exmidsbthrlem  16349