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  5702  eloprabga  5964  prfidisj  6928  djuenun  7213  addasspig  7331  mulasspig  7333  distrpig  7334  addcanpig  7335  mulcanpig  7336  ltapig  7339  distrnqg  7388  distrnq0  7460  cnegexlem2  8135  zletr  9304  zdivadd  9344  xaddass  9871  iooneg  9990  zltaddlt1le  10009  fzen  10045  fzaddel  10061  fzrev  10086  fzrevral2  10108  fzshftral  10110  fzosubel2  10197  fzonn0p1p1  10215  resqrexlemover  11021  fisum0diag2  11457  dvdsnegb  11817  muldvds1  11825  muldvds2  11826  dvdscmul  11827  dvdsmulc  11828  dvds2add  11834  dvds2sub  11835  dvdstr  11837  addmodlteqALT  11867  divalgb  11932  ndvdsadd  11938  absmulgcd  12020  rpmulgcd  12029  cncongr2  12106  hashdvds  12223  pythagtriplem1  12267  mulgmodid  13027  nmzsubg  13075