Theorem syl3an 1280

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 1184	. 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 978

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 980

This theorem is referenced by:  syl2an3an  1298  funtpg  5269  ftpg  5703  eloprabga  5965  prfidisj  6929  djuenun  7214  addasspig  7332  mulasspig  7334  distrpig  7335  addcanpig  7336  mulcanpig  7337  ltapig  7340  distrnqg  7389  distrnq0  7461  cnegexlem2  8136  zletr  9305  zdivadd  9345  xaddass  9872  iooneg  9991  zltaddlt1le  10010  fzen  10046  fzaddel  10062  fzrev  10087  fzrevral2  10109  fzshftral  10111  fzosubel2  10198  fzonn0p1p1  10216  resqrexlemover  11022  fisum0diag2  11458  dvdsnegb  11818  muldvds1  11826  muldvds2  11827  dvdscmul  11828  dvdsmulc  11829  dvds2add  11835  dvds2sub  11836  dvdstr  11838  addmodlteqALT  11868  divalgb  11933  ndvdsadd  11939  absmulgcd  12021  rpmulgcd  12030  cncongr2  12107  hashdvds  12224  pythagtriplem1  12268  mulgmodid  13028  nmzsubg  13076