Theorem syl3an 1291

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 1186	. 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 980

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 982

This theorem is referenced by:  syl2an3an  1310  funtpg  5324  ftpg  5767  eloprabga  6031  prfidisj  7023  djuenun  7323  addasspig  7442  mulasspig  7444  distrpig  7445  addcanpig  7446  mulcanpig  7447  ltapig  7450  distrnqg  7499  distrnq0  7571  cnegexlem2  8247  zletr  9421  zdivadd  9461  xaddass  9990  iooneg  10109  zltaddlt1le  10128  fzen  10164  fzaddel  10180  fzrev  10205  fzrevral2  10227  fzshftral  10229  fzosubel2  10322  fzonn0p1p1  10340  resqrexlemover  11292  fisum0diag2  11729  dvdsnegb  12090  muldvds1  12098  muldvds2  12099  dvdscmul  12100  dvdsmulc  12101  dvds2add  12107  dvds2sub  12108  dvdstr  12110  addmodlteqALT  12141  divalgb  12207  ndvdsadd  12213  absmulgcd  12309  rpmulgcd  12318  cncongr2  12397  hashdvds  12514  pythagtriplem1  12559  mulgmodid  13468  nmzsubg  13517