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  3753  relcnvtr  5186  relresfld  5196  relcoi1  5198  funco  5295  foimacnv  5519  fvi  5615  isoini2  5863  ovidig  6037  smores2  6349  tfrlem5  6369  snnen2og  6917  phpm  6923  fict  6926  infnfi  6953  isinfinf  6955  exmidpw  6966  difinfinf  7162  enumct  7176  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  isumz  11535  fsumsersdc  11541  isumclim  11567  isumclim3  11569  zprodap0  11727  alzdvds  11999  zsupcl  12087  infssuzex  12089  gcddvds  12103  dvdslegcd  12104  pclemub  12428  ennnfonelemj0  12561  ennnfonelemg  12563  ennnfonelemrn  12579  ctinf  12590  strle1g  12727  fnpr2ob  12926  metrest  14685  dvef  14906  bj-charfunbi  15373  pw1nct  15563  nnsf  15565  exmidsbthrlem  15582