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  5305  ftpg  5742  eloprabga  6005  prfidisj  6983  djuenun  7272  addasspig  7390  mulasspig  7392  distrpig  7393  addcanpig  7394  mulcanpig  7395  ltapig  7398  distrnqg  7447  distrnq0  7519  cnegexlem2  8195  zletr  9366  zdivadd  9406  xaddass  9935  iooneg  10054  zltaddlt1le  10073  fzen  10109  fzaddel  10125  fzrev  10150  fzrevral2  10172  fzshftral  10174  fzosubel2  10262  fzonn0p1p1  10280  resqrexlemover  11154  fisum0diag2  11590  dvdsnegb  11951  muldvds1  11959  muldvds2  11960  dvdscmul  11961  dvdsmulc  11962  dvds2add  11968  dvds2sub  11969  dvdstr  11971  addmodlteqALT  12001  divalgb  12066  ndvdsadd  12072  absmulgcd  12154  rpmulgcd  12163  cncongr2  12242  hashdvds  12359  pythagtriplem1  12403  mulgmodid  13231  nmzsubg  13280