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  3807  relcnvtr  5256  relresfld  5266  relcoi1  5268  funco  5366  foimacnv  5601  fvi  5703  isoini2  5960  ovidig  6139  smores2  6460  tfrlem5  6480  snnen2og  7045  phpm  7052  fict  7055  infnfi  7084  isinfinf  7086  exmidpw  7100  difinfinf  7300  enumct  7314  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  zsupcl  10492  infssuzex  10494  pfxccatin12lem3  11317  isumz  11955  fsumsersdc  11961  isumclim  11987  isumclim3  11989  zprodap0  12147  alzdvds  12420  bitsfzolem  12520  gcddvds  12539  dvdslegcd  12540  pclemub  12865  ennnfonelemj0  13027  ennnfonelemg  13029  ennnfonelemrn  13045  ctinf  13056  strle1g  13194  fnpr2ob  13428  metrest  15236  dvef  15457  umgrnloop2  16008  umgrclwwlkge2  16259  bj-charfunbi  16432  pw1nct  16630  nnsf  16633  exmidsbthrlem  16652