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:  snssg  3766  relcnvtr  5201  relresfld  5211  relcoi1  5213  funco  5310  foimacnv  5539  fvi  5635  isoini2  5887  ovidig  6062  smores2  6379  tfrlem5  6399  snnen2og  6955  phpm  6961  fict  6964  infnfi  6991  isinfinf  6993  exmidpw  7004  difinfinf  7202  enumct  7216  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  zsupcl  10372  infssuzex  10374  isumz  11671  fsumsersdc  11677  isumclim  11703  isumclim3  11705  zprodap0  11863  alzdvds  12136  bitsfzolem  12236  gcddvds  12255  dvdslegcd  12256  pclemub  12581  ennnfonelemj0  12743  ennnfonelemg  12745  ennnfonelemrn  12761  ctinf  12772  strle1g  12909  fnpr2ob  13143  metrest  14949  dvef  15170  bj-charfunbi  15709  pw1nct  15902  nnsf  15904  exmidsbthrlem  15923