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  5388  ftpg  5846  eloprabga  6118  prfidisj  7162  djuenun  7470  addasspig  7593  mulasspig  7595  distrpig  7596  addcanpig  7597  mulcanpig  7598  ltapig  7601  distrnqg  7650  distrnq0  7722  cnegexlem2  8397  zletr  9573  zdivadd  9613  xaddass  10148  iooneg  10267  zltaddlt1le  10287  fzen  10323  fzaddel  10339  fzrev  10364  fzrevral2  10386  fzshftral  10388  fzosubel2  10486  fzonn0p1p1  10504  swrdf  11285  pfxccatin12lem4  11356  resqrexlemover  11633  fisum0diag2  12071  dvdsnegb  12432  muldvds1  12440  muldvds2  12441  dvdscmul  12442  dvdsmulc  12443  dvds2add  12449  dvds2sub  12450  dvdstr  12452  addmodlteqALT  12483  divalgb  12549  ndvdsadd  12555  absmulgcd  12651  rpmulgcd  12660  cncongr2  12739  hashdvds  12856  pythagtriplem1  12901  mulgmodid  13811  nmzsubg  13860  psrbagconf1o  14757  clwwlknccat  16347