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  10674  infssuzex  10676  pfxccatin12lem3  11518  isumz  12172  fsumsersdc  12178  isumclim  12204  isumclim3  12206  zprodap0  12364  alzdvds  12637  bitsfzolem  12737  gcddvds  12756  dvdslegcd  12757  pclemub  13086  ballotfilemfc0  13281  ballotfilemfcc  13282  ennnfonelemj0  13341  ennnfonelemg  13343  ennnfonelemrn  13359  ctinf  13370  strle1g  13509  fnpr2ob  13710  metrest  15656  dvef  15877  umgrnloop2  16490  umgrclwwlkge2  16741  bj-charfunbi  16935  pw1nct  17131  nnsf  17146  exmidsbthrlem  17165