Definition df-3an 1089

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 1087	. 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  1095  3anan32  1097  3ancomb  1099  3anidm  1104  3an4anass  1105  3ioran  1106  3ianor  1107  3impa  1110  3expa  1119  3jca  1129  3anbi123i  1156  3pm3.2i  1341  3jaob  1429  3anbi123d  1439  3anim123d  1446  an6  1448  an3andi  1485  an33rean  1486  cadan  1611  19.26-3an  1874  nf3and  1900  nf3an  1903  4exdistr  1963  sb3an  2087  eeeanv  2355  mopick2  2638  r19.26-3  3099  r3al  3176  r3ex  3177  rexlimdvvva  3196  3reeanv  3211  ceqsex3v  3484  ceqsex4v  3485  ceqsex8v  3487  rspc4v  3585  sbc3an  3794  elin3  4147  rexdifpr  4604  raltpg  4643  tpss  4781  opthprneg  4809  dfopif  4814  disjxun  5084  otth2  5429  otthg  5431  oteqex  5446  poirr  5542  po3nr  5545  wefrc  5616  otelxp  5666  rabxp  5670  f1orn  6782  2f1fvneq  7206  fpropnf1  7213  dff1o6  7221  oprabidw  7389  oprabid  7390  oprabv  7418  ndmovass  7546  elovmpo  7603  elovmporab  7604  elovmporab1w  7605  elovmporab1  7606  elovmpt3rab1  7618  dfwe2  7719  opiota  8003  dfxp3  8005  bropopvvv  8031  poxp2  8084  xpord2pred  8086  xpord3pred  8093  sexp3  8094  oaord  8473  oeeu  8530  nnaord  8546  naddasslem1  8621  swoso  8669  fiint  9228  funsnfsupp  9296  ttrclselem2  9636  alephval3  10021  ingru  10727  axgroth3  10743  ltrelxr  11194  ltxrlt  11204  wloglei  11670  sup2  12099  rexuz2  12813  ltxr  13030  elixx3g  13275  ixxun  13278  dfrp2  13311  elioo4g  13323  elioopnf  13360  elioomnf  13361  elicopnf  13362  elxrge0  13374  divelunit  13411  elfz2  13431  elfzuzb  13435  uzsplit  13513  fznn0  13536  elfzmlbp  13556  preduz  13567  elfzo2  13579  fzolb2  13583  fzouzsplit  13611  ssfzo12bi  13678  fzind2  13705  hashgt23el  14348  ccatsymb  14507  swrdsbslen  14589  swrdspsleq  14590  swrdccatin2  14653  pfxccatin12lem2  14655  pfxccatin12lem3  14656  pfxccatin12  14657  pfxccat3a  14662  repsdf2  14702  repswsymball  14703  repswsymballbi  14704  repswswrd  14708  s3eq3seq  14863  wrdl3s3  14886  s3sndisj  14891  s3iunsndisj  14892  abs2dif  15257  sinltx  16115  divalglem8  16328  divalglem10  16330  divalgb  16332  bitsval2  16353  divgcdz  16439  rplpwr  16486  cncongr1  16595  pythagtriplem2  16746  pythagtrip  16763  prmgaplem4  16983  isstruct  17080  setsstruct2  17102  imasvscafn  17459  xpscf  17487  mreexmrid  17567  iscatd2  17605  issect  17678  issect2  17679  oppcsect  17703  isfunc  17789  funcpropd  17827  fucsect  17900  fucinv  17901  initoeu2  17941  setcsect  18014  setcinv  18015  issgrpd  18656  ismhm0  18716  issubm2  18730  issubg3  19078  resgrpisgrp  19081  eqgval  19110  eqger  19111  cycsubgcl  19139  isgim  19195  gim0to0  19202  gaorb  19240  gaorber  19241  gastacos  19243  symg2bas  19326  galactghm  19337  pmtr3ncom  19408  ispgp  19525  efgcpbllema  19687  efgcpbllemb  19688  eqgabl  19767  qusecsub  19768  cygabl  19824  dprdw  19945  omndmul2  20066  rnglz  20104  rngpropd  20113  ringpropd  20227  ringrghm  20252  isirred2  20359  rngcsect  20571  rngcinv  20572  ringcsect  20605  ringcinv  20606  drngid2  20687  issdrg2  20730  isorng  20796  islss  20887  islmim  21016  lmhmpropd  21027  zndvds  21506  znleval  21511  znleval2  21512  obselocv  21685  mpfrcl  22041  matinvgcell  22378  mat1dimscm  22418  scmatscm  22456  scmatf1  22474  mdetunilem7  22561  cpmatacl  22659  cpmatmcl  22662  mat2pmatf1  22672  mat2pmatghm  22673  mat2pmatmul  22674  mat2pmatlin  22678  mat2pmatscmxcl  22683  m2pmfzgsumcl  22691  decpmataa0  22711  monmatcollpw  22722  pmatcollpwscmatlem1  22732  pmatcollpwscmatlem2  22733  pm2mpghm  22759  pm2mpmhmlem2  22762  monmat2matmon  22767  chfacfisf  22797  chfacfisfcpmat  22798  chfacfpmmulgsum2  22808  isbasis3g  22892  leordtvallem2  23154  lmfval  23175  lmbr  23201  lmbr2  23202  lmmo  23323  dfconn2  23362  ptbasin  23520  ptbasfi  23524  txcnpi  23551  ptcnp  23565  hausdiag  23588  qtophmeo  23760  fbunfip  23812  elflim2  23907  hausflimi  23923  isfcls  23952  isfcls2  23956  istmd  24017  istgp  24020  istrg  24107  istdrg  24109  istdrg2  24121  istlm  24128  imasdsf1olem  24316  xmeterval  24375  xmeter  24376  prdsxmslem2  24472  blval2  24505  isngp  24539  isngp2  24540  isngp3  24541  isnlm  24618  cnbl0  24716  cnblcld  24717  elii1  24880  isphtpc  24939  phtpcer  24940  isclmp  25042  iscph  25115  lmmbr  25203  lmmbr2  25204  lmmbrf  25207  iscfil2  25211  iscau3  25223  iscau4  25224  iscauf  25225  caucfil  25228  isbn  25283  ishl2  25315  ovolfcl  25411  ioombl1lem4  25506  mbfmax  25594  iblpos  25738  limcrcl  25819  ig1pval3  26124  ulmdvlem3  26351  ellogdm  26588  relogbcl  26723  fsumvma2  27165  chpchtsum  27170  chpub  27171  dchrelbas3  27189  gausslemma2dlem1a  27316  noetalem1  27693  sltssnb  27749  eqcuts  27765  eqcuts2  27766  lnhl  28671  colopp  28825  dfcgra2  28886  axeuclidlem  29019  axeuclid  29020  edgupgr  29191  umgr2edg1  29268  subusgr  29346  nbgrel  29397  nb3grpr2  29440  nb3gr2nb  29441  isuvtx  29452  nbupgruvtxres  29464  iscplgredg  29474  cplgr3v  29492  rusgrpropedg  29642  rgrusgrprc  29647  rusgrprc  29648  upgriswlk  29698  wlkonprop  29714  wksonproplem  29760  usgr2pth0  29822  isclwlke  29834  crctcshtrl  29880  iswwlksnx  29897  wwlknbp  29899  2trld  29995  rusgrnumwwlkl1  30028  rusgrnumwwlkb0  30031  rusgrnumwwlk  30035  clwlkclwwlkflem  30063  erclwwlkref  30079  clwwlkwwlksb  30113  erclwwlknref  30128  clwwlknon2x  30162  0wlk  30175  3spthd  30235  umgr3v3e3cycl  30243  frgr3v  30334  1to3vfriswmgr  30339  frgr2wwlkeu  30386  numclwwlk1lem2fo  30417  dlwwlknondlwlknonf1o  30424  nvex  30671  isnv  30672  dfadj2  31945  cnvadj  31952  adjeq  31995  eleigvec  32017  eleigvec2  32018  chirredi  32454  or3di  32517  tpssg  32596  eliccelico  32840  pmtrprfv2  33154  fzto1st  33169  psgnfzto1st  33171  qusker  33414  qusxpid  33428  lsmsnorb  33456  prmidl0  33515  mxidlirred  33537  ply1degltel  33659  ply1degleel  33660  eulerpartlemv  34514  eulerpartlemd  34516  eulerpartlemn  34531  prob01  34563  probun  34569  bnj170  34847  bnj248  34849  bnj252  34852  bnj253  34853  bnj945  34922  bnj1098  34932  bnj1224  34949  bnj150  35024  bnj153  35028  bnj545  35043  bnj557  35049  bnj571  35054  bnj594  35060  bnj864  35070  bnj865  35071  bnj849  35073  bnj964  35091  bnj986  35103  bnj996  35104  bnj1033  35117  bnj1110  35130  bnj1128  35138  bnj1174  35151  subgrwlk  35320  cusgr3cyclex  35324  loop1cycl  35325  2cycl2d  35327  pconnconn  35419  resconn  35434  iscvm  35447  cvmlift2lem12  35502  cvmlift3lem5  35511  satfdm  35557  elmpst  35724  mpstrcl  35729  lediv2aALT  35865  3jcadALT  35875  dfso3  35908  br6  35945  elfuns  36101  brimg  36123  lemsuccf  36127  cgrxfr  36243  segcon2  36293  seglecgr12im  36298  seglecgr12  36299  segletr  36302  btwnoutside  36313  broutsideof3  36314  outsideoftr  36317  outsidele  36320  bj-imn3ani  36850  relowlpssretop  37676  wl-df3-3mintru2  37798  lindsenlbs  37927  matunitlindflem2  37929  fdc  38057  isbnd3b  38097  ablo4pnp  38192  crngm4  38315  isidlc  38327  pridl  38349  ispridl2  38350  ispridlc  38382  ts3an1  38462  ts3an2  38463  ts3an3  38464  brres2  38585  disjressuc2  38723  xrninxp  38727  dfsuccl4  38786  dfeqvrels2  38984  dfeqvrel2  38986  dfeqvrel3  38987  dfeldisj3  39123  islshpsm  39417  islshpat  39454  cmtfvalN  39647  cmtvalN  39648  ishlat1  39789  ishlat2  39790  3dim0  39894  2dim  39907  islvol5  40016  lhpexle3  40449  cdleme0ex2N  40661  cdleme0nex  40727  cdlemg2cex  41028  cdlemg33b0  41138  cdlemg33b  41144  cdlemg33c  41145  cdlemg33e  41147  dib1dim  41602  diblsmopel  41608  dihopelvalcpre  41685  lcfls1c  41973  aks6d1c1p1  42538  aks6d1c1p1rcl  42539  sn-sup2  42935  sn-isghm  43105  3anrabdioph  43213  fgraphxp  43635  omge2  43729  faosnf0.11b  43857  dfsucon  43953  pren2  43983  dfrtrcl5  44059  brfvrcld2  44122  df3an2  44199  dfvd3  45021  3impexpVD  45285  modelaxreplem1  45408  rfcnnnub  45470  stoweidlem35  46467  smflimlem4  47206  ndmaovass  47640  nltle2tri  47747  elfz2z  47749  prproropf1olem0  47936  reuprpr  47957  gboge9  48198  sbgoldbalt  48215  nnsum4primesodd  48230  nnsum4primesoddALTV  48231  bgoldbtbndlem4  48242  bgoldbtbnd  48243  dfvopnbgr2  48287  isuspgrim  48330  isubgr3stgrlem7  48406  grlimprop2  48420  uhgrimgrlim  48421  pgn4cyclex  48560  rngcsectALTV  48709  rngcinvALTV  48710  ringcsectALTV  48743  ringcinvALTV  48744  islindeps  48887  islindeps2  48917  isldepslvec2  48919  elbigo2  48986  line2ylem  49185  io1ii  49354  catprsc  49446  0funcglem  49516  0funclem  49519  catcsect  49831  isthincd2  49870  thincsect  49900  2arwcatlem1  50028