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  3812  relcnvtr  5263  relresfld  5273  relcoi1  5275  funco  5373  foimacnv  5610  fvi  5712  isoini2  5970  ovidig  6149  smores2  6503  tfrlem5  6523  snnen2og  7088  phpm  7095  fict  7098  infnfi  7127  isinfinf  7129  exmidpw  7143  difinfinf  7343  enumct  7357  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  zsupcl  10537  infssuzex  10539  pfxccatin12lem3  11362  isumz  12013  fsumsersdc  12019  isumclim  12045  isumclim3  12047  zprodap0  12205  alzdvds  12478  bitsfzolem  12578  gcddvds  12597  dvdslegcd  12598  pclemub  12923  ennnfonelemj0  13085  ennnfonelemg  13087  ennnfonelemrn  13103  ctinf  13114  strle1g  13252  fnpr2ob  13486  metrest  15300  dvef  15521  umgrnloop2  16075  umgrclwwlkge2  16326  bj-charfunbi  16510  pw1nct  16708  nnsf  16714  exmidsbthrlem  16733