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  3807  relcnvtr  5256  relresfld  5266  relcoi1  5268  funco  5366  foimacnv  5601  fvi  5703  isoini2  5959  ovidig  6138  smores2  6459  tfrlem5  6479  snnen2og  7044  phpm  7051  fict  7054  infnfi  7083  isinfinf  7085  exmidpw  7099  difinfinf  7299  enumct  7313  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  zsupcl  10490  infssuzex  10492  pfxccatin12lem3  11312  isumz  11949  fsumsersdc  11955  isumclim  11981  isumclim3  11983  zprodap0  12141  alzdvds  12414  bitsfzolem  12514  gcddvds  12533  dvdslegcd  12534  pclemub  12859  ennnfonelemj0  13021  ennnfonelemg  13023  ennnfonelemrn  13039  ctinf  13050  strle1g  13188  fnpr2ob  13422  metrest  15229  dvef  15450  umgrnloop2  16001  umgrclwwlkge2  16252  bj-charfunbi  16406  pw1nct  16604  nnsf  16607  exmidsbthrlem  16626