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  3833  relcnvtr  5287  relresfld  5297  relcoi1  5299  funco  5397  foimacnv  5637  fvi  5739  isoini2  5998  ovidig  6179  smores2  6538  tfrlem5  6558  snnen2og  7126  phpm  7133  fict  7136  infnfi  7165  isinfinf  7167  exmidpw  7181  difinfinf  7405  enumct  7419  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  zsupcl  10613  infssuzex  10615  pfxccatin12lem3  11449  isumz  12100  fsumsersdc  12106  isumclim  12132  isumclim3  12134  zprodap0  12292  alzdvds  12565  bitsfzolem  12665  gcddvds  12684  dvdslegcd  12685  pclemub  13010  ballotfilemfc0  13176  ballotfilemfcc  13177  ennnfonelemj0  13236  ennnfonelemg  13238  ennnfonelemrn  13254  ctinf  13265  strle1g  13403  fnpr2ob  13604  metrest  15497  dvef  15718  umgrnloop2  16272  umgrclwwlkge2  16523  bj-charfunbi  16707  pw1nct  16903  nnsf  16909  exmidsbthrlem  16928