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  3844  relcnvtr  5302  relresfld  5312  relcoi1  5314  funco  5412  foimacnv  5652  fvi  5754  isoini2  6015  ovidig  6196  smores2  6555  tfrlem5  6575  snnen2og  7150  phpm  7157  fict  7160  infnfi  7189  isinfinf  7191  exmidpw  7205  difinfinf  7431  enumct  7445  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  zsupcl  10642  infssuzex  10644  pfxccatin12lem3  11482  isumz  12134  fsumsersdc  12140  isumclim  12166  isumclim3  12168  zprodap0  12326  alzdvds  12599  bitsfzolem  12699  gcddvds  12718  dvdslegcd  12719  pclemub  13044  ballotfilemfc0  13210  ballotfilemfcc  13211  ennnfonelemj0  13270  ennnfonelemg  13272  ennnfonelemrn  13288  ctinf  13299  strle1g  13437  fnpr2ob  13638  metrest  15530  dvef  15751  umgrnloop2  16306  umgrclwwlkge2  16557  bj-charfunbi  16751  pw1nct  16947  nnsf  16953  exmidsbthrlem  16972