Theorem syl3an 1320

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 1215	. 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 )

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syl2an3an  1339  funtpg  5432  ftpg  5899  eloprabga  6175  prfidisj  7234  djuenun  7568  addasspig  7697  mulasspig  7699  distrpig  7700  addcanpig  7701  mulcanpig  7702  ltapig  7705  distrnqg  7754  distrnq0  7826  cnegexlem2  8503  zletr  9698  zdivadd  9739  xaddass  10281  iooneg  10400  zltaddlt1le  10420  fzen  10457  fzaddel  10475  fzrev  10501  fzrevral2  10523  fzshftral  10525  fzosubel2  10623  fzonn0p1p1  10641  swrdf  11441  pfxccatin12lem4  11512  resqrexlemover  11790  fisum0diag2  12230  dvdsnegb  12591  muldvds1  12599  muldvds2  12600  dvdscmul  12601  dvdsmulc  12602  dvds2add  12608  dvds2sub  12609  dvdstr  12611  addmodlteqALT  12642  divalgb  12708  ndvdsadd  12714  absmulgcd  12810  rpmulgcd  12819  cncongr2  12898  hashdvds  13019  pythagtriplem1  13064  mulgmodid  14013  nmzsubg  14062  assa2ass  15058  psrbagconf1o  15113  clwwlknccat  16762