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  5307  relresfld  5317  relcoi1  5319  funco  5417  foimacnv  5657  fvi  5760  isoini2  6025  ovidig  6206  smores2  6565  tfrlem5  6585  snnen2og  7160  phpm  7167  fict  7170  infnfi  7199  isinfinf  7201  exmidpw  7215  difinfinf  7441  enumct  7455  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  zsupcl  10664  infssuzex  10666  pfxccatin12lem3  11504  isumz  12156  fsumsersdc  12162  isumclim  12188  isumclim3  12190  zprodap0  12348  alzdvds  12621  bitsfzolem  12721  gcddvds  12740  dvdslegcd  12741  pclemub  13066  ballotfilemfc0  13232  ballotfilemfcc  13233  ennnfonelemj0  13292  ennnfonelemg  13294  ennnfonelemrn  13310  ctinf  13321  strle1g  13460  fnpr2ob  13661  metrest  15607  dvef  15828  umgrnloop2  16392  umgrclwwlkge2  16643  bj-charfunbi  16837  pw1nct  17033  nnsf  17048  exmidsbthrlem  17067