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  6569  tfrlem5  6589  snnen2og  7164  phpm  7171  fict  7174  infnfi  7203  isinfinf  7205  exmidpw  7219  difinfinf  7447  enumct  7461  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  zsupcl  10681  infssuzex  10683  pfxccatin12lem3  11526  isumz  12181  fsumsersdc  12187  isumclim  12213  isumclim3  12215  zprodap0  12373  alzdvds  12646  bitsfzolem  12746  gcddvds  12765  dvdslegcd  12766  pclemub  13095  ballotfilemfc0  13290  ballotfilemfcc  13291  ennnfonelemj0  13350  ennnfonelemg  13352  ennnfonelemrn  13368  ctinf  13379  strle1g  13519  fnpr2ob  13720  metrest  15732  dvef  15953  umgrnloop2  16597  umgrclwwlkge2  16848  bj-charfunbi  17042  pw1nct  17238  nnsf  17254  exmidsbthrlem  17273