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:  relcnvtr  5102  relresfld  5112  relcoi1  5114  funco  5207  foimacnv  5429  fvi  5522  isoini2  5764  ovidig  5932  smores2  6235  tfrlem5  6255  snnen2og  6797  phpm  6803  fict  6806  infnfi  6833  isinfinf  6835  exmidpw  6846  difinfinf  7035  enumct  7049  exmidfodomrlemr  7120  exmidfodomrlemrALT  7121  isumz  11268  fsumsersdc  11274  isumclim  11300  isumclim3  11302  zprodap0  11460  alzdvds  11727  zsupcl  11815  infssuzex  11817  gcddvds  11827  dvdslegcd  11828  ennnfonelemrn  12120  ctinf  12131  strle1g  12240  metrest  12866  dvef  13048  bj-charfunbi  13346  pw1nct  13536  nnsf  13539  exmidsbthrlem  13556