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  3766  relcnvtr  5201  relresfld  5211  relcoi1  5213  funco  5310  foimacnv  5539  fvi  5635  isoini2  5887  ovidig  6062  smores2  6379  tfrlem5  6399  snnen2og  6955  phpm  6961  fict  6964  infnfi  6991  isinfinf  6993  exmidpw  7004  difinfinf  7202  enumct  7216  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  zsupcl  10372  infssuzex  10374  isumz  11642  fsumsersdc  11648  isumclim  11674  isumclim3  11676  zprodap0  11834  alzdvds  12107  bitsfzolem  12207  gcddvds  12226  dvdslegcd  12227  pclemub  12552  ennnfonelemj0  12714  ennnfonelemg  12716  ennnfonelemrn  12732  ctinf  12743  strle1g  12880  fnpr2ob  13114  metrest  14920  dvef  15141  bj-charfunbi  15680  pw1nct  15873  nnsf  15875  exmidsbthrlem  15894