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  3828  relcnvtr  5282  relresfld  5292  relcoi1  5294  funco  5392  foimacnv  5632  fvi  5734  isoini2  5992  ovidig  6171  smores2  6525  tfrlem5  6545  snnen2og  7113  phpm  7120  fict  7123  infnfi  7152  isinfinf  7154  exmidpw  7168  difinfinf  7392  enumct  7406  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  zsupcl  10591  infssuzex  10593  pfxccatin12lem3  11424  isumz  12075  fsumsersdc  12081  isumclim  12107  isumclim3  12109  zprodap0  12267  alzdvds  12540  bitsfzolem  12640  gcddvds  12659  dvdslegcd  12660  pclemub  12985  ennnfonelemj0  13152  ennnfonelemg  13154  ennnfonelemrn  13170  ctinf  13181  strle1g  13319  fnpr2ob  13553  metrest  15371  dvef  15592  umgrnloop2  16146  umgrclwwlkge2  16397  bj-charfunbi  16581  pw1nct  16777  nnsf  16783  exmidsbthrlem  16802