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  5435  ftpg  5902  eloprabga  6178  prfidisj  7238  djuenun  7574  addasspig  7703  mulasspig  7705  distrpig  7706  addcanpig  7707  mulcanpig  7708  ltapig  7711  distrnqg  7760  distrnq0  7832  cnegexlem2  8509  zletr  9705  zdivadd  9746  xaddass  10288  iooneg  10407  zltaddlt1le  10427  fzen  10464  fzaddel  10482  fzrev  10508  fzrevral2  10530  fzshftral  10532  fzosubel2  10630  fzonn0p1p1  10648  swrdf  11449  pfxccatin12lem4  11520  resqrexlemover  11798  fisum0diag2  12239  dvdsnegb  12600  muldvds1  12608  muldvds2  12609  dvdscmul  12610  dvdsmulc  12611  dvds2add  12617  dvds2sub  12618  dvdstr  12620  addmodlteqALT  12651  divalgb  12717  ndvdsadd  12723  absmulgcd  12819  rpmulgcd  12828  cncongr2  12907  hashdvds  13028  pythagtriplem1  13073  mulgmodid  14023  nmzsubg  14072  assa2ass  15118  psrbagconf1o  15174  gsumbagdiaglem  15175  psrass1filem  15177  psrass1fi  15201  clwwlknccat  16869