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  3773  relcnvtr  5211  relresfld  5221  relcoi1  5223  funco  5320  foimacnv  5552  fvi  5649  isoini2  5901  ovidig  6076  smores2  6393  tfrlem5  6413  snnen2og  6971  phpm  6977  fict  6980  infnfi  7007  isinfinf  7009  exmidpw  7020  difinfinf  7218  enumct  7232  exmidfodomrlemr  7326  exmidfodomrlemrALT  7327  zsupcl  10396  infssuzex  10398  isumz  11775  fsumsersdc  11781  isumclim  11807  isumclim3  11809  zprodap0  11967  alzdvds  12240  bitsfzolem  12340  gcddvds  12359  dvdslegcd  12360  pclemub  12685  ennnfonelemj0  12847  ennnfonelemg  12849  ennnfonelemrn  12865  ctinf  12876  strle1g  13013  fnpr2ob  13247  metrest  15053  dvef  15274  bj-charfunbi  15885  pw1nct  16081  nnsf  16083  exmidsbthrlem  16102