Theorem syl3an 1316

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 1211	. 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 1005

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 1007

This theorem is referenced by:  syl2an3an  1335  funtpg  5407  ftpg  5868  eloprabga  6140  prfidisj  7187  djuenun  7519  addasspig  7645  mulasspig  7647  distrpig  7648  addcanpig  7649  mulcanpig  7650  ltapig  7653  distrnqg  7702  distrnq0  7774  cnegexlem2  8449  zletr  9627  zdivadd  9667  xaddass  10202  iooneg  10321  zltaddlt1le  10341  fzen  10377  fzaddel  10393  fzrev  10418  fzrevral2  10440  fzshftral  10442  fzosubel2  10540  fzonn0p1p1  10558  swrdf  11347  pfxccatin12lem4  11418  resqrexlemover  11695  fisum0diag2  12133  dvdsnegb  12494  muldvds1  12502  muldvds2  12503  dvdscmul  12504  dvdsmulc  12505  dvds2add  12511  dvds2sub  12512  dvdstr  12514  addmodlteqALT  12545  divalgb  12611  ndvdsadd  12617  absmulgcd  12713  rpmulgcd  12722  cncongr2  12801  hashdvds  12918  pythagtriplem1  12963  mulgmodid  13878  nmzsubg  13927  psrbagconf1o  14828  clwwlknccat  16418