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  3805  relcnvtr  5254  relresfld  5264  relcoi1  5266  funco  5364  foimacnv  5598  fvi  5699  isoini2  5955  ovidig  6134  smores2  6455  tfrlem5  6475  snnen2og  7040  phpm  7047  fict  7050  infnfi  7077  isinfinf  7079  exmidpw  7093  difinfinf  7291  enumct  7305  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  zsupcl  10481  infssuzex  10483  pfxccatin12lem3  11303  isumz  11940  fsumsersdc  11946  isumclim  11972  isumclim3  11974  zprodap0  12132  alzdvds  12405  bitsfzolem  12505  gcddvds  12524  dvdslegcd  12525  pclemub  12850  ennnfonelemj0  13012  ennnfonelemg  13014  ennnfonelemrn  13030  ctinf  13041  strle1g  13179  fnpr2ob  13413  metrest  15220  dvef  15441  umgrnloop2  15990  umgrclwwlkge2  16197  bj-charfunbi  16342  pw1nct  16540  nnsf  16543  exmidsbthrlem  16562