Theorem syl3an 1262

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 1167	. 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 963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  syl2an3an  1280  funtpg  5223  ftpg  5653  eloprabga  5910  prfidisj  6873  djuenun  7149  addasspig  7252  mulasspig  7254  distrpig  7255  addcanpig  7256  mulcanpig  7257  ltapig  7260  distrnqg  7309  distrnq0  7381  cnegexlem2  8055  zletr  9221  zdivadd  9258  xaddass  9779  iooneg  9898  zltaddlt1le  9917  fzen  9951  fzaddel  9967  fzrev  9992  fzrevral2  10014  fzshftral  10016  fzosubel2  10103  fzonn0p1p1  10121  resqrexlemover  10921  fisum0diag2  11355  dvdsnegb  11715  muldvds1  11723  muldvds2  11724  dvdscmul  11725  dvdsmulc  11726  dvds2add  11732  dvds2sub  11733  dvdstr  11735  addmodlteqALT  11763  divalgb  11828  ndvdsadd  11834  absmulgcd  11916  rpmulgcd  11925  cncongr2  11996  hashdvds  12111  pythagtriplem1  12155