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  7442  enumct  7456  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  zsupcl  10675  infssuzex  10677  pfxccatin12lem3  11520  isumz  12175  fsumsersdc  12181  isumclim  12207  isumclim3  12209  zprodap0  12367  alzdvds  12640  bitsfzolem  12740  gcddvds  12759  dvdslegcd  12760  pclemub  13089  ballotfilemfc0  13284  ballotfilemfcc  13285  ennnfonelemj0  13344  ennnfonelemg  13346  ennnfonelemrn  13362  ctinf  13373  strle1g  13513  fnpr2ob  13714  metrest  15698  dvef  15919  umgrnloop2  16558  umgrclwwlkge2  16809  bj-charfunbi  17003  pw1nct  17199  nnsf  17214  exmidsbthrlem  17233