Definition df-3an 1087

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

This definition is referenced by:  3anass  1093  3anan32  1095  3ancomb  1097  3anidm  1102  3an4anass  1103  3ioran  1104  3ianor  1105  3impa  1108  3expa  1116  3jca  1126  3anbi123i  1153  3pm3.2i  1337  3anbi123d  1434  3anim123d  1441  an6  1443  an3andi  1480  an33rean  1481  an33reanOLD  1482  cadan  1612  19.26-3an  1876  nf3and  1902  nf3an  1905  4exdistr  1966  sb3an  2085  eeeanv  2350  mopick2  2639  r19.26-3  3096  r3al  3125  3reeanv  3293  ceqsex3v  3474  ceqsex4v  3475  ceqsex8v  3477  sbc3an  3782  elin3  4130  rexdifpr  4591  raltpg  4631  tpss  4765  opthprneg  4792  dfopif  4797  dfopifOLD  4798  disjxun  5068  otth2  5392  otthg  5394  oteqex  5408  poirr  5506  po3nr  5509  wefrc  5574  rabxp  5626  f1orn  6710  fpropnf1  7121  dff1o6  7128  oprabidw  7286  oprabid  7287  oprabv  7313  ndmovass  7438  elovmpo  7492  elovmporab  7493  elovmporab1w  7494  elovmporab1  7495  elovmpt3rab1  7507  dfwe2  7602  opiota  7872  dfxp3  7874  bropopvvv  7901  oaord  8340  oeeu  8396  nnaord  8412  swoso  8489  fiint  9021  funsnfsupp  9082  alephval3  9797  ingru  10502  axgroth3  10518  ltrelxr  10967  ltxrlt  10976  wloglei  11437  sup2  11861  rexuz2  12568  ltxr  12780  elixx3g  13021  ixxun  13024  dfrp2  13057  elioo4g  13068  elioopnf  13104  elioomnf  13105  elicopnf  13106  elxrge0  13118  divelunit  13155  elfz2  13175  elfzuzb  13179  uzsplit  13257  fznn0  13277  elfzmlbp  13296  preduz  13307  elfzo2  13319  fzolb2  13323  fzouzsplit  13350  ssfzo12bi  13410  fzind2  13433  hashgt23el  14067  ccatsymb  14215  swrdsbslen  14305  swrdspsleq  14306  swrdccatin2  14370  pfxccatin12lem2  14372  pfxccatin12lem3  14373  pfxccatin12  14374  pfxccat3a  14379  repsdf2  14419  repswsymball  14420  repswsymballbi  14421  repswswrd  14425  s3eq3seq  14580  wrdl3s3  14605  s3sndisj  14606  s3iunsndisj  14607  abs2dif  14972  sinltx  15826  divalglem8  16037  divalglem10  16039  divalgb  16041  bitsval2  16060  divgcdz  16146  rplpwr  16195  cncongr1  16300  pythagtriplem2  16446  pythagtrip  16463  prmgaplem4  16683  isstruct  16781  setsstruct2  16803  imasvscafn  17165  xpscf  17193  mreexmrid  17269  iscatd2  17307  issect  17382  issect2  17383  oppcsect  17407  isfunc  17495  funcpropd  17532  fucsect  17606  fucinv  17607  initoeu2  17647  setcsect  17720  setcinv  17721  issubm2  18358  issubg3  18688  resgrpisgrp  18691  eqgval  18720  eqger  18721  cycsubgcl  18740  isgim  18793  gaorb  18828  gaorber  18829  gastacos  18831  symg2bas  18915  galactghm  18927  pmtr3ncom  18998  ispgp  19112  efgcpbllema  19275  efgcpbllemb  19276  eqgabl  19351  cygabl  19406  dprdw  19528  ringpropd  19736  ringrghm  19759  isirred2  19858  gim0to0  19901  drngid2  19922  issdrg2  19981  islss  20111  islmim  20239  lmhmpropd  20250  zndvds  20669  znleval  20674  znleval2  20675  obselocv  20845  isassa  20973  mpfrcl  21205  matinvgcell  21492  mat1dimscm  21532  scmatscm  21570  scmatf1  21588  mdetunilem7  21675  cpmatacl  21773  cpmatmcl  21776  mat2pmatf1  21786  mat2pmatghm  21787  mat2pmatmul  21788  mat2pmatlin  21792  mat2pmatscmxcl  21797  m2pmfzgsumcl  21805  decpmataa0  21825  monmatcollpw  21836  pmatcollpwscmatlem1  21846  pmatcollpwscmatlem2  21847  pm2mpghm  21873  pm2mpmhmlem2  21876  monmat2matmon  21881  chfacfisf  21911  chfacfisfcpmat  21912  chfacfpmmulgsum2  21922  isbasis3g  22007  leordtvallem2  22270  lmfval  22291  lmbr  22317  lmbr2  22318  lmmo  22439  dfconn2  22478  ptbasin  22636  ptbasfi  22640  txcnpi  22667  ptcnp  22681  hausdiag  22704  qtophmeo  22876  fbunfip  22928  elflim2  23023  hausflimi  23039  isfcls  23068  isfcls2  23072  istmd  23133  istgp  23136  istrg  23223  istdrg  23225  istdrg2  23237  istlm  23244  imasdsf1olem  23434  xmeterval  23493  xmeter  23494  prdsxmslem2  23591  blval2  23624  isngp  23658  isngp2  23659  isngp3  23660  isnlm  23745  cnbl0  23843  cnblcld  23844  elii1  24004  isphtpc  24063  phtpcer  24064  isclmp  24166  iscph  24239  lmmbr  24327  lmmbr2  24328  lmmbrf  24331  iscfil2  24335  iscau3  24347  iscau4  24348  iscauf  24349  caucfil  24352  isbn  24407  ishl2  24439  ovolfcl  24535  ioombl1lem4  24630  mbfmax  24718  iblpos  24862  limcrcl  24943  ig1pval3  25244  ulmdvlem3  25466  ellogdm  25699  relogbcl  25828  fsumvma2  26267  chpchtsum  26272  chpub  26273  dchrelbas3  26291  gausslemma2dlem1a  26418  lnhl  26880  colopp  27034  dfcgra2  27095  axeuclidlem  27233  axeuclid  27234  edgupgr  27407  umgr2edg1  27481  subusgr  27559  nbgrel  27610  nb3grpr2  27653  nb3gr2nb  27654  isuvtx  27665  nbupgruvtxres  27677  iscplgredg  27687  cplgr3v  27705  rusgrpropedg  27854  rgrusgrprc  27859  rusgrprc  27860  upgriswlk  27910  wlkonprop  27928  wksonproplem  27974  usgr2pth0  28034  isclwlke  28046  crctcshtrl  28089  iswwlksnx  28106  wwlknbp  28108  2trld  28204  rusgrnumwwlkl1  28234  rusgrnumwwlkb0  28237  rusgrnumwwlk  28241  clwlkclwwlkflem  28269  erclwwlkref  28285  clwwlkwwlksb  28319  erclwwlknref  28334  clwwlknon2x  28368  0wlk  28381  3spthd  28441  umgr3v3e3cycl  28449  frgr3v  28540  1to3vfriswmgr  28545  frgr2wwlkeu  28592  numclwwlk1lem2fo  28623  dlwwlknondlwlknonf1o  28630  nvex  28874  isnv  28875  dfadj2  30148  cnvadj  30155  adjeq  30198  eleigvec  30220  eleigvec2  30221  chirredi  30657  or3di  30711  eliccelico  31000  omndmul2  31240  pmtrprfv2  31259  fzto1st  31272  psgnfzto1st  31274  isorng  31400  qusker  31451  qusxpid  31461  lsmsnorb  31481  prmidl0  31528  eulerpartlemv  32231  eulerpartlemd  32233  eulerpartlemn  32248  prob01  32280  probun  32286  bnj170  32577  bnj248  32579  bnj252  32582  bnj253  32583  bnj945  32653  bnj1098  32663  bnj1224  32681  bnj150  32756  bnj153  32760  bnj545  32775  bnj557  32781  bnj571  32786  bnj594  32792  bnj864  32802  bnj865  32803  bnj849  32805  bnj964  32823  bnj986  32835  bnj996  32836  bnj1033  32849  bnj1110  32862  bnj1128  32870  bnj1174  32883  subgrwlk  32994  cusgr3cyclex  32998  loop1cycl  32999  2cycl2d  33001  pconnconn  33093  resconn  33108  iscvm  33121  cvmlift2lem12  33176  cvmlift3lem5  33185  satfdm  33231  elmpst  33398  mpstrcl  33403  lediv2aALT  33535  dfso3  33566  ot2elxp  33582  br6  33630  ttrclselem2  33712  poxp2  33717  xpord2pred  33719  xpord3pred  33725  sexp3  33726  noetalem1  33871  eqscut  33926  eqscut2  33927  elfuns  34144  brimg  34166  brsuccf  34170  cgrxfr  34284  segcon2  34334  seglecgr12im  34339  seglecgr12  34340  segletr  34343  btwnoutside  34354  broutsideof3  34355  outsideoftr  34358  outsidele  34361  bj-imn3ani  34696  relowlpssretop  35462  wl-df3-3mintru2  35584  lindsenlbs  35699  matunitlindflem2  35701  fdc  35830  isbnd3b  35870  ablo4pnp  35965  crngm4  36088  isidlc  36100  pridl  36122  ispridl2  36123  ispridlc  36155  ts3an1  36235  ts3an2  36236  ts3an3  36237  brres2  36334  xrninxp  36445  dfeqvrels2  36628  dfeqvrel2  36630  dfeqvrel3  36631  dfeldisj3  36757  islshpsm  36921  islshpat  36958  cmtfvalN  37151  cmtvalN  37152  ishlat1  37293  ishlat2  37294  3dim0  37398  2dim  37411  islvol5  37520  lhpexle3  37953  cdleme0ex2N  38165  cdleme0nex  38231  cdlemg2cex  38532  cdlemg33b0  38642  cdlemg33b  38648  cdlemg33c  38649  cdlemg33e  38651  dib1dim  39106  diblsmopel  39112  dihopelvalcpre  39189  lcfls1c  39477  sn-sup2  40360  3anrabdioph  40520  fgraphxp  40952  dfsucon  41028  pren2  41049  dfrtrcl5  41126  brfvrcld2  41189  df3an2  41266  dfvd3  42100  3impexpVD  42365  rfcnnnub  42468  stoweidlem35  43466  smflimlem4  44196  ndmaovass  44585  nltle2tri  44693  elfz2z  44695  prproropf1olem0  44842  reuprpr  44863  gboge9  45104  sbgoldbalt  45121  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  bgoldbtbndlem4  45148  bgoldbtbnd  45149  ismhm0  45247  rnglz  45330  rngcsect  45426  rngcinv  45427  rngcsectALTV  45438  rngcinvALTV  45439  ringcsect  45477  ringcinv  45478  ringcsectALTV  45501  ringcinvALTV  45502  islindeps  45682  islindeps2  45712  isldepslvec2  45714  elbigo2  45786  line2ylem  45985  io1ii  46102  catprsc  46182  isthincd2  46207  thincsect  46226