Theorem syl3an 1315

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 1210	. 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 1004

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 1006

This theorem is referenced by:  syl2an3an  1334  funtpg  5381  ftpg  5838  eloprabga  6108  prfidisj  7119  djuenun  7427  addasspig  7550  mulasspig  7552  distrpig  7553  addcanpig  7554  mulcanpig  7555  ltapig  7558  distrnqg  7607  distrnq0  7679  cnegexlem2  8355  zletr  9529  zdivadd  9569  xaddass  10104  iooneg  10223  zltaddlt1le  10242  fzen  10278  fzaddel  10294  fzrev  10319  fzrevral2  10341  fzshftral  10343  fzosubel2  10441  fzonn0p1p1  10459  swrdf  11240  pfxccatin12lem4  11311  resqrexlemover  11588  fisum0diag2  12026  dvdsnegb  12387  muldvds1  12395  muldvds2  12396  dvdscmul  12397  dvdsmulc  12398  dvds2add  12404  dvds2sub  12405  dvdstr  12407  addmodlteqALT  12438  divalgb  12504  ndvdsadd  12510  absmulgcd  12606  rpmulgcd  12615  cncongr2  12694  hashdvds  12811  pythagtriplem1  12856  mulgmodid  13766  nmzsubg  13815  clwwlknccat  16293