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  1309  funtpg  5306  ftpg  5743  eloprabga  6006  prfidisj  6985  djuenun  7274  addasspig  7392  mulasspig  7394  distrpig  7395  addcanpig  7396  mulcanpig  7397  ltapig  7400  distrnqg  7449  distrnq0  7521  cnegexlem2  8197  zletr  9369  zdivadd  9409  xaddass  9938  iooneg  10057  zltaddlt1le  10076  fzen  10112  fzaddel  10128  fzrev  10153  fzrevral2  10175  fzshftral  10177  fzosubel2  10265  fzonn0p1p1  10283  resqrexlemover  11157  fisum0diag2  11593  dvdsnegb  11954  muldvds1  11962  muldvds2  11963  dvdscmul  11964  dvdsmulc  11965  dvds2add  11971  dvds2sub  11972  dvdstr  11974  addmodlteqALT  12004  divalgb  12069  ndvdsadd  12075  absmulgcd  12157  rpmulgcd  12166  cncongr2  12245  hashdvds  12362  pythagtriplem1  12406  mulgmodid  13234  nmzsubg  13283