Definition df-3an 1086

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

This definition is referenced by:  3anass  1092  3anan32  1094  3ancomb  1096  3anidm  1101  3an4anass  1102  3ioran  1103  3ianor  1104  3impa  1107  3expa  1115  3jca  1125  3anbi123i  1152  3pm3.2i  1336  3anbi123d  1432  3anim123d  1439  an6  1441  an3andi  1478  an33rean  1479  cadan  1602  19.26-3an  1867  nf3and  1893  nf3an  1896  4exdistr  1957  sb3an  2076  eeeanv  2341  mopick2  2628  r19.26-3  3108  r3al  3192  3reeanv  3223  ceqsex3v  3529  ceqsex4v  3530  ceqsex8v  3532  rspc4v  3628  sbc3an  3846  elin3  4200  rexdifpr  4664  raltpg  4705  tpss  4841  opthprneg  4868  dfopif  4873  disjxun  5148  otth2  5487  otthg  5489  oteqex  5504  poirr  5604  po3nr  5607  wefrc  5674  otelxp  5724  rabxp  5728  f1orn  6852  fpropnf1  7281  dff1o6  7288  oprabidw  7455  oprabid  7456  oprabv  7484  ndmovass  7613  elovmpo  7670  elovmporab  7671  elovmporab1w  7672  elovmporab1  7673  elovmpt3rab1  7685  dfwe2  7780  opiota  8067  dfxp3  8069  bropopvvv  8099  poxp2  8152  xpord2pred  8154  xpord3pred  8161  sexp3  8162  oaord  8572  oeeu  8628  nnaord  8644  naddasslem1  8719  swoso  8762  fiint  9354  funsnfsupp  9421  ttrclselem2  9755  alephval3  10139  ingru  10844  axgroth3  10860  ltrelxr  11311  ltxrlt  11320  wloglei  11782  sup2  12206  rexuz2  12919  ltxr  13133  elixx3g  13375  ixxun  13378  dfrp2  13411  elioo4g  13422  elioopnf  13458  elioomnf  13459  elicopnf  13460  elxrge0  13472  divelunit  13509  elfz2  13529  elfzuzb  13533  uzsplit  13611  fznn0  13631  elfzmlbp  13650  preduz  13661  elfzo2  13673  fzolb2  13677  fzouzsplit  13705  ssfzo12bi  13765  fzind2  13788  hashgt23el  14421  ccatsymb  14570  swrdsbslen  14652  swrdspsleq  14653  swrdccatin2  14717  pfxccatin12lem2  14719  pfxccatin12lem3  14720  pfxccatin12  14721  pfxccat3a  14726  repsdf2  14766  repswsymball  14767  repswsymballbi  14768  repswswrd  14772  s3eq3seq  14928  wrdl3s3  14951  s3sndisj  14952  s3iunsndisj  14953  abs2dif  15317  sinltx  16171  divalglem8  16382  divalglem10  16384  divalgb  16386  bitsval2  16405  divgcdz  16491  rplpwr  16538  cncongr1  16643  pythagtriplem2  16791  pythagtrip  16808  prmgaplem4  17028  isstruct  17126  setsstruct2  17148  imasvscafn  17524  xpscf  17552  mreexmrid  17628  iscatd2  17666  issect  17741  issect2  17742  oppcsect  17766  isfunc  17855  funcpropd  17894  fucsect  17969  fucinv  17970  initoeu2  18010  setcsect  18083  setcinv  18084  issgrpd  18695  ismhm0  18752  issubm2  18761  issubg3  19104  resgrpisgrp  19107  eqgval  19137  eqger  19138  cycsubgcl  19166  isgim  19221  gim0to0  19228  gaorb  19263  gaorber  19264  gastacos  19266  symg2bas  19352  galactghm  19364  pmtr3ncom  19435  ispgp  19552  efgcpbllema  19714  efgcpbllemb  19715  eqgabl  19794  qusecsub  19795  cygabl  19851  dprdw  19972  rnglz  20110  rngpropd  20119  ringpropd  20229  ringrghm  20254  isirred2  20365  rngcsect  20574  rngcinv  20575  ringcsect  20608  ringcinv  20609  drngid2  20650  issdrg2  20688  islss  20823  islmim  20952  lmhmpropd  20963  zndvds  21488  znleval  21493  znleval2  21494  obselocv  21667  mpfrcl  22036  matinvgcell  22355  mat1dimscm  22395  scmatscm  22433  scmatf1  22451  mdetunilem7  22538  cpmatacl  22636  cpmatmcl  22639  mat2pmatf1  22649  mat2pmatghm  22650  mat2pmatmul  22651  mat2pmatlin  22655  mat2pmatscmxcl  22660  m2pmfzgsumcl  22668  decpmataa0  22688  monmatcollpw  22699  pmatcollpwscmatlem1  22709  pmatcollpwscmatlem2  22710  pm2mpghm  22736  pm2mpmhmlem2  22739  monmat2matmon  22744  chfacfisf  22774  chfacfisfcpmat  22775  chfacfpmmulgsum2  22785  isbasis3g  22870  leordtvallem2  23133  lmfval  23154  lmbr  23180  lmbr2  23181  lmmo  23302  dfconn2  23341  ptbasin  23499  ptbasfi  23503  txcnpi  23530  ptcnp  23544  hausdiag  23567  qtophmeo  23739  fbunfip  23791  elflim2  23886  hausflimi  23902  isfcls  23931  isfcls2  23935  istmd  23996  istgp  23999  istrg  24086  istdrg  24088  istdrg2  24100  istlm  24107  imasdsf1olem  24297  xmeterval  24356  xmeter  24357  prdsxmslem2  24456  blval2  24489  isngp  24523  isngp2  24524  isngp3  24525  isnlm  24610  cnbl0  24708  cnblcld  24709  elii1  24876  isphtpc  24938  phtpcer  24939  isclmp  25042  iscph  25116  lmmbr  25204  lmmbr2  25205  lmmbrf  25208  iscfil2  25212  iscau3  25224  iscau4  25225  iscauf  25226  caucfil  25229  isbn  25284  ishl2  25316  ovolfcl  25413  ioombl1lem4  25508  mbfmax  25596  iblpos  25740  limcrcl  25821  ig1pval3  26130  ulmdvlem3  26356  ellogdm  26591  relogbcl  26723  fsumvma2  27165  chpchtsum  27170  chpub  27171  dchrelbas3  27189  gausslemma2dlem1a  27316  noetalem1  27692  eqscut  27756  eqscut2  27757  lnhl  28437  colopp  28591  dfcgra2  28652  axeuclidlem  28791  axeuclid  28792  edgupgr  28965  umgr2edg1  29042  subusgr  29120  nbgrel  29171  nb3grpr2  29214  nb3gr2nb  29215  isuvtx  29226  nbupgruvtxres  29238  iscplgredg  29248  cplgr3v  29266  rusgrpropedg  29416  rgrusgrprc  29421  rusgrprc  29422  upgriswlk  29473  wlkonprop  29490  wksonproplem  29536  wksonproplemOLD  29537  usgr2pth0  29597  isclwlke  29609  crctcshtrl  29652  iswwlksnx  29669  wwlknbp  29671  2trld  29767  rusgrnumwwlkl1  29797  rusgrnumwwlkb0  29800  rusgrnumwwlk  29804  clwlkclwwlkflem  29832  erclwwlkref  29848  clwwlkwwlksb  29882  erclwwlknref  29897  clwwlknon2x  29931  0wlk  29944  3spthd  30004  umgr3v3e3cycl  30012  frgr3v  30103  1to3vfriswmgr  30108  frgr2wwlkeu  30155  numclwwlk1lem2fo  30186  dlwwlknondlwlknonf1o  30193  nvex  30439  isnv  30440  dfadj2  31713  cnvadj  31720  adjeq  31763  eleigvec  31785  eleigvec2  31786  chirredi  32222  or3di  32277  eliccelico  32563  omndmul2  32810  pmtrprfv2  32829  fzto1st  32842  psgnfzto1st  32844  isorng  33032  qusker  33079  qusxpid  33093  lsmsnorb  33118  prmidl0  33184  mxidlirred  33203  ply1degltel  33270  ply1degleel  33271  eulerpartlemv  33989  eulerpartlemd  33991  eulerpartlemn  34006  prob01  34038  probun  34044  bnj170  34334  bnj248  34336  bnj252  34339  bnj253  34340  bnj945  34409  bnj1098  34419  bnj1224  34437  bnj150  34512  bnj153  34516  bnj545  34531  bnj557  34537  bnj571  34542  bnj594  34548  bnj864  34558  bnj865  34559  bnj849  34561  bnj964  34579  bnj986  34591  bnj996  34592  bnj1033  34605  bnj1110  34618  bnj1128  34626  bnj1174  34639  subgrwlk  34747  cusgr3cyclex  34751  loop1cycl  34752  2cycl2d  34754  pconnconn  34846  resconn  34861  iscvm  34874  cvmlift2lem12  34929  cvmlift3lem5  34938  satfdm  34984  elmpst  35151  mpstrcl  35156  lediv2aALT  35286  dfso3  35319  br6  35356  elfuns  35516  brimg  35538  brsuccf  35542  cgrxfr  35656  segcon2  35706  seglecgr12im  35711  seglecgr12  35712  segletr  35715  btwnoutside  35726  broutsideof3  35727  outsideoftr  35730  outsidele  35733  bj-imn3ani  36069  relowlpssretop  36848  wl-df3-3mintru2  36970  lindsenlbs  37093  matunitlindflem2  37095  fdc  37223  isbnd3b  37263  ablo4pnp  37358  crngm4  37481  isidlc  37493  pridl  37515  ispridl2  37516  ispridlc  37548  ts3an1  37628  ts3an2  37629  ts3an3  37630  brres2  37744  disjressuc2  37864  xrninxp  37868  dfeqvrels2  38064  dfeqvrel2  38066  dfeqvrel3  38067  dfeldisj3  38195  islshpsm  38456  islshpat  38493  cmtfvalN  38686  cmtvalN  38687  ishlat1  38828  ishlat2  38829  3dim0  38934  2dim  38947  islvol5  39056  lhpexle3  39489  cdleme0ex2N  39701  cdleme0nex  39767  cdlemg2cex  40068  cdlemg33b0  40178  cdlemg33b  40184  cdlemg33c  40185  cdlemg33e  40187  dib1dim  40642  diblsmopel  40648  dihopelvalcpre  40725  lcfls1c  41013  aks6d1c1p1  41582  aks6d1c1p1rcl  41583  sn-sup2  42027  3anrabdioph  42205  fgraphxp  42635  omge2  42730  faosnf0.11b  42860  dfsucon  42956  pren2  42986  dfrtrcl5  43062  brfvrcld2  43125  df3an2  43202  dfvd3  44033  3impexpVD  44298  rfcnnnub  44401  stoweidlem35  45425  smflimlem4  46164  ndmaovass  46588  nltle2tri  46695  elfz2z  46697  prproropf1olem0  46844  reuprpr  46865  gboge9  47106  sbgoldbalt  47123  nnsum4primesodd  47138  nnsum4primesoddALTV  47139  bgoldbtbndlem4  47150  bgoldbtbnd  47151  dfvopnbgr2  47190  rngcsectALTV  47388  rngcinvALTV  47389  ringcsectALTV  47422  ringcinvALTV  47423  islindeps  47572  islindeps2  47602  isldepslvec2  47604  elbigo2  47676  line2ylem  47875  io1ii  47990  catprsc  48070  isthincd2  48095  thincsect  48114