Theorem syl3an 1313

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 1208	. 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 1002

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 1004

This theorem is referenced by:  syl2an3an  1332  funtpg  5372  ftpg  5827  eloprabga  6097  prfidisj  7100  djuenun  7405  addasspig  7528  mulasspig  7530  distrpig  7531  addcanpig  7532  mulcanpig  7533  ltapig  7536  distrnqg  7585  distrnq0  7657  cnegexlem2  8333  zletr  9507  zdivadd  9547  xaddass  10077  iooneg  10196  zltaddlt1le  10215  fzen  10251  fzaddel  10267  fzrev  10292  fzrevral2  10314  fzshftral  10316  fzosubel2  10413  fzonn0p1p1  10431  swrdf  11202  pfxccatin12lem4  11273  resqrexlemover  11536  fisum0diag2  11973  dvdsnegb  12334  muldvds1  12342  muldvds2  12343  dvdscmul  12344  dvdsmulc  12345  dvds2add  12351  dvds2sub  12352  dvdstr  12354  addmodlteqALT  12385  divalgb  12451  ndvdsadd  12457  absmulgcd  12553  rpmulgcd  12562  cncongr2  12641  hashdvds  12758  pythagtriplem1  12803  mulgmodid  13713  nmzsubg  13762