Definition df-3an 1088

Description: Define conjunction ('and') of three wff's. Definition *4.34 of [WhiteheadRussell] p. 118. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law anass 468. (Contributed by NM, 8-Apr-1994.)

Assertion

Ref	Expression
df-3an	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))

Detailed syntax breakdown of Definition df-3an

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3		wch	. . 3 wff 𝜒
4	1, 2, 3	w3a 1086	. 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒)
5	1, 2	wa 395	. . 3 wff (𝜑 ∧ 𝜓)
6	5, 3	wa 395	. 2 wff ((𝜑 ∧ 𝜓) ∧ 𝜒)
7	4, 6	wb 206	1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))

This definition is referenced by:  3anass  1094  3anan32  1096  3ancomb  1098  3anidm  1103  3an4anass  1104  3ioran  1105  3ianor  1106  3impa  1109  3expa  1118  3jca  1128  3anbi123i  1155  3pm3.2i  1340  3jaob  1428  3anbi123d  1438  3anim123d  1445  an6  1447  an3andi  1484  an33rean  1485  cadan  1610  19.26-3an  1873  nf3and  1899  nf3an  1902  4exdistr  1962  sb3an  2084  eeeanv  2350  mopick2  2632  r19.26-3  3093  r3al  3170  r3ex  3171  rexlimdvvva  3190  3reeanv  3205  ceqsex3v  3492  ceqsex4v  3493  ceqsex8v  3495  rspc4v  3597  sbc3an  3806  elin3  4156  rexdifpr  4612  raltpg  4651  tpss  4789  opthprneg  4817  dfopif  4822  disjxun  5089  otth2  5423  otthg  5425  oteqex  5440  poirr  5536  po3nr  5539  wefrc  5610  otelxp  5660  rabxp  5664  f1orn  6773  2f1fvneq  7194  fpropnf1  7201  dff1o6  7209  oprabidw  7377  oprabid  7378  oprabv  7406  ndmovass  7534  elovmpo  7591  elovmporab  7592  elovmporab1w  7593  elovmporab1  7594  elovmpt3rab1  7606  dfwe2  7707  opiota  7991  dfxp3  7993  bropopvvv  8020  poxp2  8073  xpord2pred  8075  xpord3pred  8082  sexp3  8083  oaord  8462  oeeu  8518  nnaord  8534  naddasslem1  8609  swoso  8656  fiint  9211  funsnfsupp  9276  ttrclselem2  9616  alephval3  9998  ingru  10703  axgroth3  10719  ltrelxr  11170  ltxrlt  11180  wloglei  11646  sup2  12075  rexuz2  12794  ltxr  13011  elixx3g  13255  ixxun  13258  dfrp2  13291  elioo4g  13303  elioopnf  13340  elioomnf  13341  elicopnf  13342  elxrge0  13354  divelunit  13391  elfz2  13411  elfzuzb  13415  uzsplit  13493  fznn0  13516  elfzmlbp  13536  preduz  13547  elfzo2  13559  fzolb2  13563  fzouzsplit  13591  ssfzo12bi  13658  fzind2  13685  hashgt23el  14328  ccatsymb  14487  swrdsbslen  14569  swrdspsleq  14570  swrdccatin2  14633  pfxccatin12lem2  14635  pfxccatin12lem3  14636  pfxccatin12  14637  pfxccat3a  14642  repsdf2  14682  repswsymball  14683  repswsymballbi  14684  repswswrd  14688  s3eq3seq  14843  wrdl3s3  14866  s3sndisj  14871  s3iunsndisj  14872  abs2dif  15237  sinltx  16095  divalglem8  16308  divalglem10  16310  divalgb  16312  bitsval2  16333  divgcdz  16419  rplpwr  16466  cncongr1  16575  pythagtriplem2  16726  pythagtrip  16743  prmgaplem4  16963  isstruct  17060  setsstruct2  17082  imasvscafn  17438  xpscf  17466  mreexmrid  17546  iscatd2  17584  issect  17657  issect2  17658  oppcsect  17682  isfunc  17768  funcpropd  17806  fucsect  17879  fucinv  17880  initoeu2  17920  setcsect  17993  setcinv  17994  issgrpd  18635  ismhm0  18695  issubm2  18709  issubg3  19054  resgrpisgrp  19057  eqgval  19087  eqger  19088  cycsubgcl  19116  isgim  19172  gim0to0  19179  gaorb  19217  gaorber  19218  gastacos  19220  symg2bas  19303  galactghm  19314  pmtr3ncom  19385  ispgp  19502  efgcpbllema  19664  efgcpbllemb  19665  eqgabl  19744  qusecsub  19745  cygabl  19801  dprdw  19922  omndmul2  20043  rnglz  20081  rngpropd  20090  ringpropd  20204  ringrghm  20229  isirred2  20337  rngcsect  20549  rngcinv  20550  ringcsect  20583  ringcinv  20584  drngid2  20665  issdrg2  20708  isorng  20774  islss  20865  islmim  20994  lmhmpropd  21005  zndvds  21484  znleval  21489  znleval2  21490  obselocv  21663  mpfrcl  22018  matinvgcell  22348  mat1dimscm  22388  scmatscm  22426  scmatf1  22444  mdetunilem7  22531  cpmatacl  22629  cpmatmcl  22632  mat2pmatf1  22642  mat2pmatghm  22643  mat2pmatmul  22644  mat2pmatlin  22648  mat2pmatscmxcl  22653  m2pmfzgsumcl  22661  decpmataa0  22681  monmatcollpw  22692  pmatcollpwscmatlem1  22702  pmatcollpwscmatlem2  22703  pm2mpghm  22729  pm2mpmhmlem2  22732  monmat2matmon  22737  chfacfisf  22767  chfacfisfcpmat  22768  chfacfpmmulgsum2  22778  isbasis3g  22862  leordtvallem2  23124  lmfval  23145  lmbr  23171  lmbr2  23172  lmmo  23293  dfconn2  23332  ptbasin  23490  ptbasfi  23494  txcnpi  23521  ptcnp  23535  hausdiag  23558  qtophmeo  23730  fbunfip  23782  elflim2  23877  hausflimi  23893  isfcls  23922  isfcls2  23926  istmd  23987  istgp  23990  istrg  24077  istdrg  24079  istdrg2  24091  istlm  24098  imasdsf1olem  24286  xmeterval  24345  xmeter  24346  prdsxmslem2  24442  blval2  24475  isngp  24509  isngp2  24510  isngp3  24511  isnlm  24588  cnbl0  24686  cnblcld  24687  elii1  24856  isphtpc  24918  phtpcer  24919  isclmp  25022  iscph  25095  lmmbr  25183  lmmbr2  25184  lmmbrf  25187  iscfil2  25191  iscau3  25203  iscau4  25204  iscauf  25205  caucfil  25208  isbn  25263  ishl2  25295  ovolfcl  25392  ioombl1lem4  25487  mbfmax  25575  iblpos  25719  limcrcl  25800  ig1pval3  26108  ulmdvlem3  26336  ellogdm  26573  relogbcl  26708  fsumvma2  27150  chpchtsum  27155  chpub  27156  dchrelbas3  27174  gausslemma2dlem1a  27301  noetalem1  27678  ssltsnb  27730  eqscut  27744  eqscut2  27745  lnhl  28591  colopp  28745  dfcgra2  28806  axeuclidlem  28938  axeuclid  28939  edgupgr  29110  umgr2edg1  29187  subusgr  29265  nbgrel  29316  nb3grpr2  29359  nb3gr2nb  29360  isuvtx  29371  nbupgruvtxres  29383  iscplgredg  29393  cplgr3v  29411  rusgrpropedg  29561  rgrusgrprc  29566  rusgrprc  29567  upgriswlk  29617  wlkonprop  29633  wksonproplem  29679  usgr2pth0  29741  isclwlke  29753  crctcshtrl  29799  iswwlksnx  29816  wwlknbp  29818  2trld  29914  rusgrnumwwlkl1  29944  rusgrnumwwlkb0  29947  rusgrnumwwlk  29951  clwlkclwwlkflem  29979  erclwwlkref  29995  clwwlkwwlksb  30029  erclwwlknref  30044  clwwlknon2x  30078  0wlk  30091  3spthd  30151  umgr3v3e3cycl  30159  frgr3v  30250  1to3vfriswmgr  30255  frgr2wwlkeu  30302  numclwwlk1lem2fo  30333  dlwwlknondlwlknonf1o  30340  nvex  30586  isnv  30587  dfadj2  31860  cnvadj  31867  adjeq  31910  eleigvec  31932  eleigvec2  31933  chirredi  32369  or3di  32433  tpssg  32512  eliccelico  32755  pmtrprfv2  33052  fzto1st  33067  psgnfzto1st  33069  qusker  33309  qusxpid  33323  lsmsnorb  33351  prmidl0  33410  mxidlirred  33432  ply1degltel  33550  ply1degleel  33551  eulerpartlemv  34372  eulerpartlemd  34374  eulerpartlemn  34389  prob01  34421  probun  34427  bnj170  34705  bnj248  34707  bnj252  34710  bnj253  34711  bnj945  34780  bnj1098  34790  bnj1224  34808  bnj150  34883  bnj153  34887  bnj545  34902  bnj557  34908  bnj571  34913  bnj594  34919  bnj864  34929  bnj865  34930  bnj849  34932  bnj964  34950  bnj986  34962  bnj996  34963  bnj1033  34976  bnj1110  34989  bnj1128  34997  bnj1174  35010  subgrwlk  35164  cusgr3cyclex  35168  loop1cycl  35169  2cycl2d  35171  pconnconn  35263  resconn  35278  iscvm  35291  cvmlift2lem12  35346  cvmlift3lem5  35355  satfdm  35401  elmpst  35568  mpstrcl  35573  lediv2aALT  35709  3jcadALT  35719  dfso3  35752  br6  35789  elfuns  35948  brimg  35970  brsuccf  35974  cgrxfr  36088  segcon2  36138  seglecgr12im  36143  seglecgr12  36144  segletr  36147  btwnoutside  36158  broutsideof3  36159  outsideoftr  36162  outsidele  36165  bj-imn3ani  36620  relowlpssretop  37397  wl-df3-3mintru2  37519  lindsenlbs  37654  matunitlindflem2  37656  fdc  37784  isbnd3b  37824  ablo4pnp  37919  crngm4  38042  isidlc  38054  pridl  38076  ispridl2  38077  ispridlc  38109  ts3an1  38189  ts3an2  38190  ts3an3  38191  brres2  38302  disjressuc2  38419  xrninxp  38423  dfeqvrels2  38624  dfeqvrel2  38626  dfeqvrel3  38627  dfeldisj3  38756  islshpsm  39018  islshpat  39055  cmtfvalN  39248  cmtvalN  39249  ishlat1  39390  ishlat2  39391  3dim0  39495  2dim  39508  islvol5  39617  lhpexle3  40050  cdleme0ex2N  40262  cdleme0nex  40328  cdlemg2cex  40629  cdlemg33b0  40739  cdlemg33b  40745  cdlemg33c  40746  cdlemg33e  40748  dib1dim  41203  diblsmopel  41209  dihopelvalcpre  41286  lcfls1c  41574  aks6d1c1p1  42139  aks6d1c1p1rcl  42140  sn-sup2  42523  sn-isghm  42705  3anrabdioph  42814  fgraphxp  43236  omge2  43330  faosnf0.11b  43459  dfsucon  43555  pren2  43585  dfrtrcl5  43661  brfvrcld2  43724  df3an2  43801  dfvd3  44623  3impexpVD  44887  modelaxreplem1  45010  rfcnnnub  45072  stoweidlem35  46072  smflimlem4  46811  ndmaovass  47236  nltle2tri  47343  elfz2z  47345  prproropf1olem0  47532  reuprpr  47553  gboge9  47794  sbgoldbalt  47811  nnsum4primesodd  47826  nnsum4primesoddALTV  47827  bgoldbtbndlem4  47838  bgoldbtbnd  47839  dfvopnbgr2  47883  isuspgrim  47926  isubgr3stgrlem7  48002  grlimprop2  48016  uhgrimgrlim  48017  pgn4cyclex  48156  rngcsectALTV  48305  rngcinvALTV  48306  ringcsectALTV  48339  ringcinvALTV  48340  islindeps  48484  islindeps2  48514  isldepslvec2  48516  elbigo2  48583  line2ylem  48782  io1ii  48951  catprsc  49044  0funcglem  49114  0funclem  49117  catcsect  49429  isthincd2  49468  thincsect  49498  2arwcatlem1  49626