Theorem syl3an 1313

Description: A triple syllogism inference. (Contributed by NM, 13-May-2004.)

Hypotheses

Ref	Expression
syl3an.1	|- ( ph -> ps )
syl3an.2	|- ( ch -> th )
syl3an.3	|- ( ta -> et )
syl3an.4	|- ( ( ps /\ th /\ et ) -> ze )

Assertion

Ref	Expression
syl3an	|- ( ( ph /\ ch /\ ta ) -> ze )

Proof of Theorem syl3an

Step	Hyp	Ref	Expression
1		syl3an.1	. . 3 |- ( ph -> ps )
2		syl3an.2	. . 3 |- ( ch -> th )
3		syl3an.3	. . 3 |- ( ta -> et )
4	1, 2, 3	3anim123i 1208	. 2 |- ( ( ph /\ ch /\ ta ) -> ( ps /\ th /\ et ) )
5		syl3an.4	. 2 |- ( ( ps /\ th /\ et ) -> ze )
6	4, 5	syl 14	1 |- ( ( ph /\ ch /\ ta ) -> ze )

Syntax hints:   -> wi 4   /\ w3a 1002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  syl2an3an  1332  funtpg  5378  ftpg  5833  eloprabga  6103  prfidisj  7112  djuenun  7417  addasspig  7540  mulasspig  7542  distrpig  7543  addcanpig  7544  mulcanpig  7545  ltapig  7548  distrnqg  7597  distrnq0  7669  cnegexlem2  8345  zletr  9519  zdivadd  9559  xaddass  10094  iooneg  10213  zltaddlt1le  10232  fzen  10268  fzaddel  10284  fzrev  10309  fzrevral2  10331  fzshftral  10333  fzosubel2  10430  fzonn0p1p1  10448  swrdf  11226  pfxccatin12lem4  11297  resqrexlemover  11561  fisum0diag2  11998  dvdsnegb  12359  muldvds1  12367  muldvds2  12368  dvdscmul  12369  dvdsmulc  12370  dvds2add  12376  dvds2sub  12377  dvdstr  12379  addmodlteqALT  12410  divalgb  12476  ndvdsadd  12482  absmulgcd  12578  rpmulgcd  12587  cncongr2  12666  hashdvds  12783  pythagtriplem1  12828  mulgmodid  13738  nmzsubg  13787  clwwlknccat  16218