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  3830  relcnvtr  5284  relresfld  5294  relcoi1  5296  funco  5394  foimacnv  5634  fvi  5736  isoini2  5994  ovidig  6173  smores2  6527  tfrlem5  6547  snnen2og  7115  phpm  7122  fict  7125  infnfi  7154  isinfinf  7156  exmidpw  7170  difinfinf  7394  enumct  7408  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  zsupcl  10595  infssuzex  10597  pfxccatin12lem3  11428  isumz  12079  fsumsersdc  12085  isumclim  12111  isumclim3  12113  zprodap0  12271  alzdvds  12544  bitsfzolem  12644  gcddvds  12663  dvdslegcd  12664  pclemub  12989  ballotfilemfc0  13153  ballotfilemfcc  13154  ennnfonelemj0  13169  ennnfonelemg  13171  ennnfonelemrn  13187  ctinf  13198  strle1g  13336  fnpr2ob  13570  metrest  15388  dvef  15609  umgrnloop2  16163  umgrclwwlkge2  16414  bj-charfunbi  16598  pw1nct  16794  nnsf  16800  exmidsbthrlem  16819