Theorem syl3an 1368

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 1247	. 2 |- ( ( ph /\ ch /\ ta ) -> ( ps /\ th /\ et ) )
5		syl3an.4	. 2 |- ( ( ps /\ th /\ et ) -> ze )
6	4, 5	syl 17	1 |- ( ( ph /\ ch /\ ta ) -> ze )

Syntax hints:   -> wi 4   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  syl2an3an  1386  euelss  3914  3elpr2eq  4435  funtpg  5942  funtpgOLD  5943  fresaun  6075  fresaunres2  6076  ftpg  6423  eloprabga  6747  cdaenun  8996  addasspi  9717  mulasspi  9719  distrpi  9720  addcanpi  9721  mulcanpi  9722  ltapi  9725  lemul1  10875  ltdiv2  10909  zletr  11421  zdivadd  11448  nn01to3  11781  qdivcl  11809  maxle  12022  lemin  12023  maxlt  12024  ltmin  12025  xaddass  12079  xmulasslem3  12116  xadddilem  12124  iooneg  12292  zltaddlt1le  12324  fzen  12358  fzaddel  12375  fzadd2  12376  fzrev  12403  fzrevral2  12426  fzshftral  12428  fzosubel2  12527  fzonn0p1p1  12546  fldiv2  12660  modmulnn  12688  modcyc2  12706  prsshashgt1  13198  hashssdif  13200  ccatsymb  13366  ccatw2s1ass  13407  swrdccatin12lem1  13484  fsum0diag2  14515  binomrisefac  14773  efsub  14830  dvdsnegb  14999  muldvds1  15006  muldvds2  15007  dvdscmul  15008  dvdsmulc  15009  dvdscmulr  15010  dvdsmulcr  15011  dvds2add  15015  dvds2sub  15016  dvdstr  15018  addmodlteqALT  15047  divalglem8  15123  divalgb  15127  divalgmod  15129  divalgmodOLD  15130  ndvdsadd  15134  modgcd  15253  absmulgcd  15266  rpmulgcd  15275  cncongr2  15382  hashdvds  15480  pythagtriplem1  15521  vdwlem3  15687  ressinbas  15936  gsumws2  17379  mulgmodid  17581  nmzsubg  17635  pmtr3ncomlem1  17893  pmtrdifellem1  17896  subcmn  18242  gexexlem  18255  lsmcom  18261  zaddablx  18275  assa2ass  19322  psrbagconf1o  19374  gsumbagdiaglem  19375  psrass1lem  19377  psrass1  19405  mplmonmul  19464  ply1opprmul  19609  coe1mul  19640  psgnghm  19926  2ndcdisj2  21260  fbssfi  21641  isfcf  21838  nmotri  22543  nghmplusg  22544  0nmhm  22559  iundisj2  23317  ovolioo  23336  uniiccdif  23346  basellem9  24815  cplgr2vpr  26329  redwlk  26569  frgrwopreglem5a  27175  lnocoi  27612  ipasslem5  27690  hhssabloilem  28118  hhssnv  28121  shscli  28176  shmodsi  28248  lnopmi  28859  lnopcoi  28862  cnlnadjlem2  28927  adjmul  28951  leopmul2i  28994  leoptr  28996  pjimai  29035  mdslle1i  29176  mdslle2i  29177  mdslj1i  29178  mdslj2i  29179  mdslmd1lem1  29184  mdslmd2i  29189  atexch  29240  atcvatlem  29244  chirredlem3  29251  sumdmdii  29274  sumdmdlem  29277  cdj3i  29300  iundisj2f  29403  iundisj2fi  29556  xrge0omnd  29711  bnj1384  31100  noetalem5  31867  cgr3permute3  32154  cgr3permute1  32155  cgr3com  32160  nndivsub  32456  mblfinlem2  33447  cnambfre  33458  ftc1anclem5  33489  fzmul  33537  isismty  33600  heibor1  33609  heiborlem3  33612  hlatjcl  34653  hlatjcom  34654  hlatlej1  34661  hlrelat5N  34687  2lplnmN  34845  2llnmj  34846  2lplnmj  34908  elmapresaun  37334  elmapresaunres2  37335  fzneg  37549  lsmfgcl  37644  trelded  38781  jaoded  38782  el123  38991  suctrALT  39061  suctrALTcf  39158  ltsubsubaddltsub  41315  fmtnoprmfac2lem1  41478  gboge9  41652  bgoldbtbndlem3  41695  nnsgrp  41817  c0snghm  41916  2zrngALT  41948  nn0sumltlt  42128  gsumpr  42139  lincsum  42218  dignn0fr  42395  dignn0flhalflem2  42410