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  5837  eloprabga  6107  prfidisj  7118  djuenun  7426  addasspig  7549  mulasspig  7551  distrpig  7552  addcanpig  7553  mulcanpig  7554  ltapig  7557  distrnqg  7606  distrnq0  7678  cnegexlem2  8354  zletr  9528  zdivadd  9568  xaddass  10103  iooneg  10222  zltaddlt1le  10241  fzen  10277  fzaddel  10293  fzrev  10318  fzrevral2  10340  fzshftral  10342  fzosubel2  10439  fzonn0p1p1  10457  swrdf  11235  pfxccatin12lem4  11306  resqrexlemover  11570  fisum0diag2  12007  dvdsnegb  12368  muldvds1  12376  muldvds2  12377  dvdscmul  12378  dvdsmulc  12379  dvds2add  12385  dvds2sub  12386  dvdstr  12388  addmodlteqALT  12419  divalgb  12485  ndvdsadd  12491  absmulgcd  12587  rpmulgcd  12596  cncongr2  12675  hashdvds  12792  pythagtriplem1  12837  mulgmodid  13747  nmzsubg  13796  clwwlknccat  16273