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 469. (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 396	. . 3 wff (𝜑 ∧ 𝜓)
6	5, 3	wa 396	. 2 wff ((𝜑 ∧ 𝜓) ∧ 𝜒)
7	4, 6	wb 205	1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))

This definition is referenced by:  3anass  1094  3anan32  1096  3ancomb  1098  3anidm  1103  3an4anass  1104  3ioran  1105  3ianor  1106  3impa  1109  3expa  1117  3jca  1127  3anbi123i  1154  3pm3.2i  1338  3anbi123d  1435  3anim123d  1442  an6  1444  an3andi  1481  an33rean  1482  an33reanOLD  1483  cadan  1607  19.26-3an  1872  nf3and  1898  nf3an  1901  4exdistr  1962  sb3an  2081  eeeanv  2345  mopick2  2636  r19.26-3  3111  r3al  3157  3reeanv  3294  ceqsex3v  3483  ceqsex4v  3484  ceqsex8v  3486  sbc3an  3785  elin3  4133  rexdifpr  4593  raltpg  4633  tpss  4767  opthprneg  4794  dfopif  4799  dfopifOLD  4800  disjxun  5071  otth2  5397  otthg  5399  oteqex  5413  poirr  5514  po3nr  5517  wefrc  5582  rabxp  5634  f1orn  6733  fpropnf1  7147  dff1o6  7154  oprabidw  7313  oprabid  7314  oprabv  7342  ndmovass  7467  elovmpo  7521  elovmporab  7522  elovmporab1w  7523  elovmporab1  7524  elovmpt3rab1  7536  dfwe2  7631  opiota  7906  dfxp3  7908  bropopvvv  7937  oaord  8385  oeeu  8441  nnaord  8457  swoso  8538  fiint  9098  funsnfsupp  9159  ttrclselem2  9491  alephval3  9873  ingru  10578  axgroth3  10594  ltrelxr  11043  ltxrlt  11052  wloglei  11514  sup2  11938  rexuz2  12646  ltxr  12858  elixx3g  13099  ixxun  13102  dfrp2  13135  elioo4g  13146  elioopnf  13182  elioomnf  13183  elicopnf  13184  elxrge0  13196  divelunit  13233  elfz2  13253  elfzuzb  13257  uzsplit  13335  fznn0  13355  elfzmlbp  13374  preduz  13385  elfzo2  13397  fzolb2  13401  fzouzsplit  13429  ssfzo12bi  13489  fzind2  13512  hashgt23el  14146  ccatsymb  14294  swrdsbslen  14384  swrdspsleq  14385  swrdccatin2  14449  pfxccatin12lem2  14451  pfxccatin12lem3  14452  pfxccatin12  14453  pfxccat3a  14458  repsdf2  14498  repswsymball  14499  repswsymballbi  14500  repswswrd  14504  s3eq3seq  14659  wrdl3s3  14684  s3sndisj  14685  s3iunsndisj  14686  abs2dif  15051  sinltx  15905  divalglem8  16116  divalglem10  16118  divalgb  16120  bitsval2  16139  divgcdz  16225  rplpwr  16274  cncongr1  16379  pythagtriplem2  16525  pythagtrip  16542  prmgaplem4  16762  isstruct  16860  setsstruct2  16882  imasvscafn  17255  xpscf  17283  mreexmrid  17359  iscatd2  17397  issect  17472  issect2  17473  oppcsect  17497  isfunc  17586  funcpropd  17623  fucsect  17697  fucinv  17698  initoeu2  17738  setcsect  17811  setcinv  17812  issubm2  18450  issubg3  18780  resgrpisgrp  18783  eqgval  18812  eqger  18813  cycsubgcl  18832  isgim  18885  gaorb  18920  gaorber  18921  gastacos  18923  symg2bas  19007  galactghm  19019  pmtr3ncom  19090  ispgp  19204  efgcpbllema  19367  efgcpbllemb  19368  eqgabl  19443  cygabl  19498  dprdw  19620  ringpropd  19828  ringrghm  19851  isirred2  19950  gim0to0  19993  drngid2  20014  issdrg2  20073  islss  20203  islmim  20331  lmhmpropd  20342  zndvds  20764  znleval  20769  znleval2  20770  obselocv  20942  isassa  21070  mpfrcl  21302  matinvgcell  21591  mat1dimscm  21631  scmatscm  21669  scmatf1  21687  mdetunilem7  21774  cpmatacl  21872  cpmatmcl  21875  mat2pmatf1  21885  mat2pmatghm  21886  mat2pmatmul  21887  mat2pmatlin  21891  mat2pmatscmxcl  21896  m2pmfzgsumcl  21904  decpmataa0  21924  monmatcollpw  21935  pmatcollpwscmatlem1  21945  pmatcollpwscmatlem2  21946  pm2mpghm  21972  pm2mpmhmlem2  21975  monmat2matmon  21980  chfacfisf  22010  chfacfisfcpmat  22011  chfacfpmmulgsum2  22021  isbasis3g  22106  leordtvallem2  22369  lmfval  22390  lmbr  22416  lmbr2  22417  lmmo  22538  dfconn2  22577  ptbasin  22735  ptbasfi  22739  txcnpi  22766  ptcnp  22780  hausdiag  22803  qtophmeo  22975  fbunfip  23027  elflim2  23122  hausflimi  23138  isfcls  23167  isfcls2  23171  istmd  23232  istgp  23235  istrg  23322  istdrg  23324  istdrg2  23336  istlm  23343  imasdsf1olem  23533  xmeterval  23592  xmeter  23593  prdsxmslem2  23692  blval2  23725  isngp  23759  isngp2  23760  isngp3  23761  isnlm  23846  cnbl0  23944  cnblcld  23945  elii1  24105  isphtpc  24164  phtpcer  24165  isclmp  24267  iscph  24341  lmmbr  24429  lmmbr2  24430  lmmbrf  24433  iscfil2  24437  iscau3  24449  iscau4  24450  iscauf  24451  caucfil  24454  isbn  24509  ishl2  24541  ovolfcl  24637  ioombl1lem4  24732  mbfmax  24820  iblpos  24964  limcrcl  25045  ig1pval3  25346  ulmdvlem3  25568  ellogdm  25801  relogbcl  25930  fsumvma2  26369  chpchtsum  26374  chpub  26375  dchrelbas3  26393  gausslemma2dlem1a  26520  lnhl  26983  colopp  27137  dfcgra2  27198  axeuclidlem  27337  axeuclid  27338  edgupgr  27511  umgr2edg1  27585  subusgr  27663  nbgrel  27714  nb3grpr2  27757  nb3gr2nb  27758  isuvtx  27769  nbupgruvtxres  27781  iscplgredg  27791  cplgr3v  27809  rusgrpropedg  27958  rgrusgrprc  27963  rusgrprc  27964  upgriswlk  28015  wlkonprop  28033  wksonproplem  28079  wksonproplemOLD  28080  usgr2pth0  28140  isclwlke  28152  crctcshtrl  28195  iswwlksnx  28212  wwlknbp  28214  2trld  28310  rusgrnumwwlkl1  28340  rusgrnumwwlkb0  28343  rusgrnumwwlk  28347  clwlkclwwlkflem  28375  erclwwlkref  28391  clwwlkwwlksb  28425  erclwwlknref  28440  clwwlknon2x  28474  0wlk  28487  3spthd  28547  umgr3v3e3cycl  28555  frgr3v  28646  1to3vfriswmgr  28651  frgr2wwlkeu  28698  numclwwlk1lem2fo  28729  dlwwlknondlwlknonf1o  28736  nvex  28980  isnv  28981  dfadj2  30254  cnvadj  30261  adjeq  30304  eleigvec  30326  eleigvec2  30327  chirredi  30763  or3di  30817  eliccelico  31105  omndmul2  31345  pmtrprfv2  31364  fzto1st  31377  psgnfzto1st  31379  isorng  31505  qusker  31556  qusxpid  31566  lsmsnorb  31586  prmidl0  31633  eulerpartlemv  32338  eulerpartlemd  32340  eulerpartlemn  32355  prob01  32387  probun  32393  bnj170  32684  bnj248  32686  bnj252  32689  bnj253  32690  bnj945  32760  bnj1098  32770  bnj1224  32788  bnj150  32863  bnj153  32867  bnj545  32882  bnj557  32888  bnj571  32893  bnj594  32899  bnj864  32909  bnj865  32910  bnj849  32912  bnj964  32930  bnj986  32942  bnj996  32943  bnj1033  32956  bnj1110  32969  bnj1128  32977  bnj1174  32990  subgrwlk  33101  cusgr3cyclex  33105  loop1cycl  33106  2cycl2d  33108  pconnconn  33200  resconn  33215  iscvm  33228  cvmlift2lem12  33283  cvmlift3lem5  33292  satfdm  33338  elmpst  33505  mpstrcl  33510  lediv2aALT  33642  dfso3  33671  ot2elxp  33686  br6  33731  poxp2  33797  xpord2pred  33799  xpord3pred  33805  sexp3  33806  noetalem1  33951  eqscut  34006  eqscut2  34007  elfuns  34224  brimg  34246  brsuccf  34250  cgrxfr  34364  segcon2  34414  seglecgr12im  34419  seglecgr12  34420  segletr  34423  btwnoutside  34434  broutsideof3  34435  outsideoftr  34438  outsidele  34441  bj-imn3ani  34776  relowlpssretop  35542  wl-df3-3mintru2  35664  lindsenlbs  35779  matunitlindflem2  35781  fdc  35910  isbnd3b  35950  ablo4pnp  36045  crngm4  36168  isidlc  36180  pridl  36202  ispridl2  36203  ispridlc  36235  ts3an1  36315  ts3an2  36316  ts3an3  36317  brres2  36413  xrninxp  36523  dfeqvrels2  36706  dfeqvrel2  36708  dfeqvrel3  36709  dfeldisj3  36835  islshpsm  36999  islshpat  37036  cmtfvalN  37229  cmtvalN  37230  ishlat1  37371  ishlat2  37372  3dim0  37476  2dim  37489  islvol5  37598  lhpexle3  38031  cdleme0ex2N  38243  cdleme0nex  38309  cdlemg2cex  38610  cdlemg33b0  38720  cdlemg33b  38726  cdlemg33c  38727  cdlemg33e  38729  dib1dim  39184  diblsmopel  39190  dihopelvalcpre  39267  lcfls1c  39555  sn-sup2  40444  3anrabdioph  40609  fgraphxp  41041  dfsucon  41135  pren2  41165  dfrtrcl5  41242  brfvrcld2  41305  df3an2  41382  dfvd3  42216  3impexpVD  42481  rfcnnnub  42584  stoweidlem35  43592  smflimlem4  44329  ndmaovass  44719  nltle2tri  44826  elfz2z  44828  prproropf1olem0  44975  reuprpr  44996  gboge9  45237  sbgoldbalt  45254  nnsum4primesodd  45269  nnsum4primesoddALTV  45270  bgoldbtbndlem4  45281  bgoldbtbnd  45282  ismhm0  45380  rnglz  45463  rngcsect  45559  rngcinv  45560  rngcsectALTV  45571  rngcinvALTV  45572  ringcsect  45610  ringcinv  45611  ringcsectALTV  45634  ringcinvALTV  45635  islindeps  45815  islindeps2  45845  isldepslvec2  45847  elbigo2  45919  line2ylem  46118  io1ii  46235  catprsc  46315  isthincd2  46340  thincsect  46359