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  5216  relresfld  5226  relcoi1  5228  funco  5325  foimacnv  5557  fvi  5654  isoini2  5906  ovidig  6081  smores2  6398  tfrlem5  6418  snnen2og  6976  phpm  6983  fict  6986  infnfi  7013  isinfinf  7015  exmidpw  7026  difinfinf  7224  enumct  7238  exmidfodomrlemr  7336  exmidfodomrlemrALT  7337  zsupcl  10406  infssuzex  10408  isumz  11785  fsumsersdc  11791  isumclim  11817  isumclim3  11819  zprodap0  11977  alzdvds  12250  bitsfzolem  12350  gcddvds  12369  dvdslegcd  12370  pclemub  12695  ennnfonelemj0  12857  ennnfonelemg  12859  ennnfonelemrn  12875  ctinf  12886  strle1g  13023  fnpr2ob  13257  metrest  15063  dvef  15284  umgrnloop2  15825  bj-charfunbi  15916  pw1nct  16112  nnsf  16114  exmidsbthrlem  16133