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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  relcnvtr  4994  relresfld  5004  relcoi1  5006  funco  5099  foimacnv  5319  fvi  5410  isoini2  5652  ovidig  5820  smores2  6121  tfrlem5  6141  snnen2og  6682  phpm  6688  fict  6691  infnfi  6718  isinfinf  6720  exmidpw  6731  difinfinf  6901  enumct  6914  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968  isumz  10997  fsumsersdc  11003  isumclim  11029  isumclim3  11031  alzdvds  11347  zsupcl  11435  infssuzex  11437  gcddvds  11447  dvdslegcd  11448  ennnfonelemrn  11724  ctinf  11735  strle1g  11831  metrest  12434  nnsf  12783  exmidsbthrlem  12801