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  5132  relresfld  5142  relcoi1  5144  funco  5240  foimacnv  5463  fvi  5557  isoini2  5802  ovidig  5974  smores2  6277  tfrlem5  6297  snnen2og  6841  phpm  6847  fict  6850  infnfi  6877  isinfinf  6879  exmidpw  6890  difinfinf  7082  enumct  7096  exmidfodomrlemr  7183  exmidfodomrlemrALT  7184  isumz  11356  fsumsersdc  11362  isumclim  11388  isumclim3  11390  zprodap0  11548  alzdvds  11818  zsupcl  11906  infssuzex  11908  gcddvds  11922  dvdslegcd  11923  pclemub  12245  ennnfonelemrn  12378  ctinf  12389  strle1g  12512  metrest  13385  dvef  13567  bj-charfunbi  13931  pw1nct  14121  nnsf  14123  exmidsbthrlem  14139