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  7569  addasspig  7698  mulasspig  7700  distrpig  7701  addcanpig  7702  mulcanpig  7703  ltapig  7706  distrnqg  7755  distrnq0  7827  cnegexlem2  8504  zletr  9699  zdivadd  9740  xaddass  10282  iooneg  10401  zltaddlt1le  10421  fzen  10458  fzaddel  10476  fzrev  10502  fzrevral2  10524  fzshftral  10526  fzosubel2  10624  fzonn0p1p1  10642  swrdf  11443  pfxccatin12lem4  11514  resqrexlemover  11792  fisum0diag2  12233  dvdsnegb  12594  muldvds1  12602  muldvds2  12603  dvdscmul  12604  dvdsmulc  12605  dvds2add  12611  dvds2sub  12612  dvdstr  12614  addmodlteqALT  12645  divalgb  12711  ndvdsadd  12717  absmulgcd  12813  rpmulgcd  12822  cncongr2  12901  hashdvds  13022  pythagtriplem1  13067  mulgmodid  14017  nmzsubg  14066  assa2ass  15093  psrbagconf1o  15149  clwwlknccat  16830