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 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 1084	. 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  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  2340  mopick2  2627  r19.26-3  3106  r3al  3190  3reeanv  3221  ceqsex3v  3526  ceqsex4v  3527  ceqsex8v  3529  rspc4v  3625  sbc3an  3842  elin3  4195  rexdifpr  4656  raltpg  4697  tpss  4833  opthprneg  4860  dfopif  4865  disjxun  5139  otth2  5476  otthg  5478  oteqex  5493  poirr  5593  po3nr  5596  wefrc  5663  otelxp  5713  rabxp  5717  f1orn  6836  fpropnf1  7261  dff1o6  7268  oprabidw  7435  oprabid  7436  oprabv  7464  ndmovass  7591  elovmpo  7647  elovmporab  7648  elovmporab1w  7649  elovmporab1  7650  elovmpt3rab1  7662  dfwe2  7757  opiota  8041  dfxp3  8043  bropopvvv  8073  poxp2  8126  xpord2pred  8128  xpord3pred  8135  sexp3  8136  oaord  8545  oeeu  8601  nnaord  8617  naddasslem1  8692  swoso  8735  fiint  9323  funsnfsupp  9386  ttrclselem2  9720  alephval3  10104  ingru  10809  axgroth3  10825  ltrelxr  11276  ltxrlt  11285  wloglei  11747  sup2  12171  rexuz2  12884  ltxr  13098  elixx3g  13340  ixxun  13343  dfrp2  13376  elioo4g  13387  elioopnf  13423  elioomnf  13424  elicopnf  13425  elxrge0  13437  divelunit  13474  elfz2  13494  elfzuzb  13498  uzsplit  13576  fznn0  13596  elfzmlbp  13615  preduz  13626  elfzo2  13638  fzolb2  13642  fzouzsplit  13670  ssfzo12bi  13730  fzind2  13753  hashgt23el  14387  ccatsymb  14536  swrdsbslen  14618  swrdspsleq  14619  swrdccatin2  14683  pfxccatin12lem2  14685  pfxccatin12lem3  14686  pfxccatin12  14687  pfxccat3a  14692  repsdf2  14732  repswsymball  14733  repswsymballbi  14734  repswswrd  14738  s3eq3seq  14894  wrdl3s3  14917  s3sndisj  14918  s3iunsndisj  14919  abs2dif  15283  sinltx  16137  divalglem8  16348  divalglem10  16350  divalgb  16352  bitsval2  16371  divgcdz  16457  rplpwr  16504  cncongr1  16609  pythagtriplem2  16757  pythagtrip  16774  prmgaplem4  16994  isstruct  17092  setsstruct2  17114  imasvscafn  17490  xpscf  17518  mreexmrid  17594  iscatd2  17632  issect  17707  issect2  17708  oppcsect  17732  isfunc  17821  funcpropd  17860  fucsect  17935  fucinv  17936  initoeu2  17976  setcsect  18049  setcinv  18050  issgrpd  18661  ismhm0  18718  issubm2  18727  issubg3  19069  resgrpisgrp  19072  eqgval  19102  eqger  19103  cycsubgcl  19130  isgim  19185  gim0to0  19192  gaorb  19221  gaorber  19222  gastacos  19224  symg2bas  19310  galactghm  19322  pmtr3ncom  19393  ispgp  19510  efgcpbllema  19672  efgcpbllemb  19673  eqgabl  19752  qusecsub  19753  cygabl  19809  dprdw  19930  rnglz  20068  rngpropd  20077  ringpropd  20185  ringrghm  20210  isirred2  20321  rngcsect  20530  rngcinv  20531  ringcsect  20564  ringcinv  20565  drngid2  20606  issdrg2  20644  islss  20779  islmim  20908  lmhmpropd  20919  zndvds  21440  znleval  21445  znleval2  21446  obselocv  21619  mpfrcl  21986  matinvgcell  22288  mat1dimscm  22328  scmatscm  22366  scmatf1  22384  mdetunilem7  22471  cpmatacl  22569  cpmatmcl  22572  mat2pmatf1  22582  mat2pmatghm  22583  mat2pmatmul  22584  mat2pmatlin  22588  mat2pmatscmxcl  22593  m2pmfzgsumcl  22601  decpmataa0  22621  monmatcollpw  22632  pmatcollpwscmatlem1  22642  pmatcollpwscmatlem2  22643  pm2mpghm  22669  pm2mpmhmlem2  22672  monmat2matmon  22677  chfacfisf  22707  chfacfisfcpmat  22708  chfacfpmmulgsum2  22718  isbasis3g  22803  leordtvallem2  23066  lmfval  23087  lmbr  23113  lmbr2  23114  lmmo  23235  dfconn2  23274  ptbasin  23432  ptbasfi  23436  txcnpi  23463  ptcnp  23477  hausdiag  23500  qtophmeo  23672  fbunfip  23724  elflim2  23819  hausflimi  23835  isfcls  23864  isfcls2  23868  istmd  23929  istgp  23932  istrg  24019  istdrg  24021  istdrg2  24033  istlm  24040  imasdsf1olem  24230  xmeterval  24289  xmeter  24290  prdsxmslem2  24389  blval2  24422  isngp  24456  isngp2  24457  isngp3  24458  isnlm  24543  cnbl0  24641  cnblcld  24642  elii1  24809  isphtpc  24871  phtpcer  24872  isclmp  24975  iscph  25049  lmmbr  25137  lmmbr2  25138  lmmbrf  25141  iscfil2  25145  iscau3  25157  iscau4  25158  iscauf  25159  caucfil  25162  isbn  25217  ishl2  25249  ovolfcl  25346  ioombl1lem4  25441  mbfmax  25529  iblpos  25673  limcrcl  25754  ig1pval3  26063  ulmdvlem3  26289  ellogdm  26524  relogbcl  26656  fsumvma2  27098  chpchtsum  27103  chpub  27104  dchrelbas3  27122  gausslemma2dlem1a  27249  noetalem1  27625  eqscut  27689  eqscut2  27690  lnhl  28370  colopp  28524  dfcgra2  28585  axeuclidlem  28724  axeuclid  28725  edgupgr  28898  umgr2edg1  28972  subusgr  29050  nbgrel  29101  nb3grpr2  29144  nb3gr2nb  29145  isuvtx  29156  nbupgruvtxres  29168  iscplgredg  29178  cplgr3v  29196  rusgrpropedg  29346  rgrusgrprc  29351  rusgrprc  29352  upgriswlk  29403  wlkonprop  29420  wksonproplem  29466  wksonproplemOLD  29467  usgr2pth0  29527  isclwlke  29539  crctcshtrl  29582  iswwlksnx  29599  wwlknbp  29601  2trld  29697  rusgrnumwwlkl1  29727  rusgrnumwwlkb0  29730  rusgrnumwwlk  29734  clwlkclwwlkflem  29762  erclwwlkref  29778  clwwlkwwlksb  29812  erclwwlknref  29827  clwwlknon2x  29861  0wlk  29874  3spthd  29934  umgr3v3e3cycl  29942  frgr3v  30033  1to3vfriswmgr  30038  frgr2wwlkeu  30085  numclwwlk1lem2fo  30116  dlwwlknondlwlknonf1o  30123  nvex  30369  isnv  30370  dfadj2  31643  cnvadj  31650  adjeq  31693  eleigvec  31715  eleigvec2  31716  chirredi  32152  or3di  32206  eliccelico  32493  omndmul2  32734  pmtrprfv2  32753  fzto1st  32766  psgnfzto1st  32768  isorng  32920  qusker  32967  qusxpid  32982  lsmsnorb  33007  prmidl0  33075  mxidlirred  33094  ply1degltel  33170  ply1degleel  33171  eulerpartlemv  33893  eulerpartlemd  33895  eulerpartlemn  33910  prob01  33942  probun  33948  bnj170  34238  bnj248  34240  bnj252  34243  bnj253  34244  bnj945  34313  bnj1098  34323  bnj1224  34341  bnj150  34416  bnj153  34420  bnj545  34435  bnj557  34441  bnj571  34446  bnj594  34452  bnj864  34462  bnj865  34463  bnj849  34465  bnj964  34483  bnj986  34495  bnj996  34496  bnj1033  34509  bnj1110  34522  bnj1128  34530  bnj1174  34543  subgrwlk  34651  cusgr3cyclex  34655  loop1cycl  34656  2cycl2d  34658  pconnconn  34750  resconn  34765  iscvm  34778  cvmlift2lem12  34833  cvmlift3lem5  34842  satfdm  34888  elmpst  35055  mpstrcl  35060  lediv2aALT  35190  dfso3  35223  br6  35260  elfuns  35420  brimg  35442  brsuccf  35446  cgrxfr  35560  segcon2  35610  seglecgr12im  35615  seglecgr12  35616  segletr  35619  btwnoutside  35630  broutsideof3  35631  outsideoftr  35634  outsidele  35637  bj-imn3ani  35973  relowlpssretop  36752  wl-df3-3mintru2  36874  lindsenlbs  36994  matunitlindflem2  36996  fdc  37124  isbnd3b  37164  ablo4pnp  37259  crngm4  37382  isidlc  37394  pridl  37416  ispridl2  37417  ispridlc  37449  ts3an1  37529  ts3an2  37530  ts3an3  37531  brres2  37647  disjressuc2  37769  xrninxp  37773  dfeqvrels2  37969  dfeqvrel2  37971  dfeqvrel3  37972  dfeldisj3  38100  islshpsm  38361  islshpat  38398  cmtfvalN  38591  cmtvalN  38592  ishlat1  38733  ishlat2  38734  3dim0  38839  2dim  38852  islvol5  38961  lhpexle3  39394  cdleme0ex2N  39606  cdleme0nex  39672  cdlemg2cex  39973  cdlemg33b0  40083  cdlemg33b  40089  cdlemg33c  40090  cdlemg33e  40092  dib1dim  40547  diblsmopel  40553  dihopelvalcpre  40630  lcfls1c  40918  aks6d1c1p1  41482  aks6d1c1p1rcl  41483  sn-sup2  41901  3anrabdioph  42079  fgraphxp  42510  omge2  42605  faosnf0.11b  42735  dfsucon  42831  pren2  42861  dfrtrcl5  42937  brfvrcld2  43000  df3an2  43077  dfvd3  43909  3impexpVD  44174  rfcnnnub  44277  stoweidlem35  45304  smflimlem4  46043  ndmaovass  46467  nltle2tri  46574  elfz2z  46576  prproropf1olem0  46723  reuprpr  46744  gboge9  46985  sbgoldbalt  47002  nnsum4primesodd  47017  nnsum4primesoddALTV  47018  bgoldbtbndlem4  47029  bgoldbtbnd  47030  rngcsectALTV  47206  rngcinvALTV  47207  ringcsectALTV  47240  ringcinvALTV  47241  islindeps  47390  islindeps2  47420  isldepslvec2  47422  elbigo2  47494  line2ylem  47693  io1ii  47808  catprsc  47888  isthincd2  47913  thincsect  47932