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 )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  snssg  3849  relcnvtr  5310  relresfld  5320  relcoi1  5322  funco  5420  foimacnv  5660  fvi  5763  isoini2  6028  ovidig  6209  smores2  6570  tfrlem5  6590  snnen2og  7166  phpm  7173  fict  7176  infnfi  7205  isinfinf  7207  exmidpw  7221  difinfinf  7447  enumct  7461  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  zsupcl  10680  infssuzex  10682  pfxccatin12lem3  11525  isumz  12180  fsumsersdc  12186  isumclim  12212  isumclim3  12214  zprodap0  12372  alzdvds  12645  bitsfzolem  12745  gcddvds  12764  dvdslegcd  12765  pclemub  13094  ballotfilemfc0  13289  ballotfilemfcc  13290  ennnfonelemj0  13349  ennnfonelemg  13351  ennnfonelemrn  13367  ctinf  13378  strle1g  13518  fnpr2ob  13719  metrest  15749  dvef  15970  umgrnloop2  16614  umgrclwwlkge2  16865  bj-charfunbi  17059  pw1nct  17255  nnsf  17271  exmidsbthrlem  17290