Definition df-3an 1090

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

This definition is referenced by:  3anass  1096  3anan32  1098  3ancomb  1100  3anidm  1105  3an4anass  1106  3ioran  1107  3ianor  1108  3impa  1111  3expa  1119  3jca  1129  3anbi123i  1156  3pm3.2i  1340  3anbi123d  1437  3anim123d  1444  an6  1446  an3andi  1483  an33rean  1484  an33reanOLD  1485  cadan  1611  19.26-3an  1876  nf3and  1902  nf3an  1905  4exdistr  1966  sb3an  2085  eeeanv  2347  mopick2  2634  r19.26-3  3113  r3al  3197  3reeanv  3228  ceqsex3v  3532  ceqsex4v  3533  ceqsex8v  3535  rspc4v  3630  sbc3an  3847  elin3  4200  rexdifpr  4661  raltpg  4702  tpss  4838  opthprneg  4865  dfopif  4870  disjxun  5146  otth2  5483  otthg  5485  oteqex  5500  poirr  5600  po3nr  5603  wefrc  5670  otelxp  5719  rabxp  5723  f1orn  6841  fpropnf1  7263  dff1o6  7270  oprabidw  7437  oprabid  7438  oprabv  7466  ndmovass  7592  elovmpo  7648  elovmporab  7649  elovmporab1w  7650  elovmporab1  7651  elovmpt3rab1  7663  dfwe2  7758  opiota  8042  dfxp3  8044  bropopvvv  8073  poxp2  8126  xpord2pred  8128  xpord3pred  8135  sexp3  8136  oaord  8544  oeeu  8600  nnaord  8616  naddasslem1  8690  swoso  8733  fiint  9321  funsnfsupp  9384  ttrclselem2  9718  alephval3  10102  ingru  10807  axgroth3  10823  ltrelxr  11272  ltxrlt  11281  wloglei  11743  sup2  12167  rexuz2  12880  ltxr  13092  elixx3g  13334  ixxun  13337  dfrp2  13370  elioo4g  13381  elioopnf  13417  elioomnf  13418  elicopnf  13419  elxrge0  13431  divelunit  13468  elfz2  13488  elfzuzb  13492  uzsplit  13570  fznn0  13590  elfzmlbp  13609  preduz  13620  elfzo2  13632  fzolb2  13636  fzouzsplit  13664  ssfzo12bi  13724  fzind2  13747  hashgt23el  14381  ccatsymb  14529  swrdsbslen  14611  swrdspsleq  14612  swrdccatin2  14676  pfxccatin12lem2  14678  pfxccatin12lem3  14679  pfxccatin12  14680  pfxccat3a  14685  repsdf2  14725  repswsymball  14726  repswsymballbi  14727  repswswrd  14731  s3eq3seq  14887  wrdl3s3  14910  s3sndisj  14911  s3iunsndisj  14912  abs2dif  15276  sinltx  16129  divalglem8  16340  divalglem10  16342  divalgb  16344  bitsval2  16363  divgcdz  16449  rplpwr  16496  cncongr1  16601  pythagtriplem2  16747  pythagtrip  16764  prmgaplem4  16984  isstruct  17082  setsstruct2  17104  imasvscafn  17480  xpscf  17508  mreexmrid  17584  iscatd2  17622  issect  17697  issect2  17698  oppcsect  17722  isfunc  17811  funcpropd  17848  fucsect  17922  fucinv  17923  initoeu2  17963  setcsect  18036  setcinv  18037  issgrpd  18618  issubm2  18682  issubg3  19019  resgrpisgrp  19022  eqgval  19052  eqger  19053  cycsubgcl  19078  isgim  19131  gaorb  19166  gaorber  19167  gastacos  19169  symg2bas  19255  galactghm  19267  pmtr3ncom  19338  ispgp  19455  efgcpbllema  19617  efgcpbllemb  19618  eqgabl  19697  qusecsub  19698  cygabl  19754  dprdw  19875  ringpropd  20096  ringrghm  20119  isirred2  20228  gim0to0  20274  drngid2  20329  issdrg2  20404  islss  20538  islmim  20666  lmhmpropd  20677  zndvds  21097  znleval  21102  znleval2  21103  obselocv  21275  mpfrcl  21640  matinvgcell  21929  mat1dimscm  21969  scmatscm  22007  scmatf1  22025  mdetunilem7  22112  cpmatacl  22210  cpmatmcl  22213  mat2pmatf1  22223  mat2pmatghm  22224  mat2pmatmul  22225  mat2pmatlin  22229  mat2pmatscmxcl  22234  m2pmfzgsumcl  22242  decpmataa0  22262  monmatcollpw  22273  pmatcollpwscmatlem1  22283  pmatcollpwscmatlem2  22284  pm2mpghm  22310  pm2mpmhmlem2  22313  monmat2matmon  22318  chfacfisf  22348  chfacfisfcpmat  22349  chfacfpmmulgsum2  22359  isbasis3g  22444  leordtvallem2  22707  lmfval  22728  lmbr  22754  lmbr2  22755  lmmo  22876  dfconn2  22915  ptbasin  23073  ptbasfi  23077  txcnpi  23104  ptcnp  23118  hausdiag  23141  qtophmeo  23313  fbunfip  23365  elflim2  23460  hausflimi  23476  isfcls  23505  isfcls2  23509  istmd  23570  istgp  23573  istrg  23660  istdrg  23662  istdrg2  23674  istlm  23681  imasdsf1olem  23871  xmeterval  23930  xmeter  23931  prdsxmslem2  24030  blval2  24063  isngp  24097  isngp2  24098  isngp3  24099  isnlm  24184  cnbl0  24282  cnblcld  24283  elii1  24443  isphtpc  24502  phtpcer  24503  isclmp  24605  iscph  24679  lmmbr  24767  lmmbr2  24768  lmmbrf  24771  iscfil2  24775  iscau3  24787  iscau4  24788  iscauf  24789  caucfil  24792  isbn  24847  ishl2  24879  ovolfcl  24975  ioombl1lem4  25070  mbfmax  25158  iblpos  25302  limcrcl  25383  ig1pval3  25684  ulmdvlem3  25906  ellogdm  26139  relogbcl  26268  fsumvma2  26707  chpchtsum  26712  chpub  26713  dchrelbas3  26731  gausslemma2dlem1a  26858  noetalem1  27234  eqscut  27296  eqscut2  27297  lnhl  27856  colopp  28010  dfcgra2  28071  axeuclidlem  28210  axeuclid  28211  edgupgr  28384  umgr2edg1  28458  subusgr  28536  nbgrel  28587  nb3grpr2  28630  nb3gr2nb  28631  isuvtx  28642  nbupgruvtxres  28654  iscplgredg  28664  cplgr3v  28682  rusgrpropedg  28831  rgrusgrprc  28836  rusgrprc  28837  upgriswlk  28888  wlkonprop  28905  wksonproplem  28951  wksonproplemOLD  28952  usgr2pth0  29012  isclwlke  29024  crctcshtrl  29067  iswwlksnx  29084  wwlknbp  29086  2trld  29182  rusgrnumwwlkl1  29212  rusgrnumwwlkb0  29215  rusgrnumwwlk  29219  clwlkclwwlkflem  29247  erclwwlkref  29263  clwwlkwwlksb  29297  erclwwlknref  29312  clwwlknon2x  29346  0wlk  29359  3spthd  29419  umgr3v3e3cycl  29427  frgr3v  29518  1to3vfriswmgr  29523  frgr2wwlkeu  29570  numclwwlk1lem2fo  29601  dlwwlknondlwlknonf1o  29608  nvex  29852  isnv  29853  dfadj2  31126  cnvadj  31133  adjeq  31176  eleigvec  31198  eleigvec2  31199  chirredi  31635  or3di  31689  eliccelico  31976  omndmul2  32218  pmtrprfv2  32237  fzto1st  32250  psgnfzto1st  32252  isorng  32406  qusker  32453  qusxpid  32464  lsmsnorb  32490  prmidl0  32558  mxidlirred  32577  ply1degltel  32655  eulerpartlemv  33352  eulerpartlemd  33354  eulerpartlemn  33369  prob01  33401  probun  33407  bnj170  33698  bnj248  33700  bnj252  33703  bnj253  33704  bnj945  33773  bnj1098  33783  bnj1224  33801  bnj150  33876  bnj153  33880  bnj545  33895  bnj557  33901  bnj571  33906  bnj594  33912  bnj864  33922  bnj865  33923  bnj849  33925  bnj964  33943  bnj986  33955  bnj996  33956  bnj1033  33969  bnj1110  33982  bnj1128  33990  bnj1174  34003  subgrwlk  34112  cusgr3cyclex  34116  loop1cycl  34117  2cycl2d  34119  pconnconn  34211  resconn  34226  iscvm  34239  cvmlift2lem12  34294  cvmlift3lem5  34303  satfdm  34349  elmpst  34516  mpstrcl  34521  lediv2aALT  34651  dfso3  34678  br6  34716  elfuns  34876  brimg  34898  brsuccf  34902  cgrxfr  35016  segcon2  35066  seglecgr12im  35071  seglecgr12  35072  segletr  35075  btwnoutside  35086  broutsideof3  35087  outsideoftr  35090  outsidele  35093  bj-imn3ani  35454  relowlpssretop  36234  wl-df3-3mintru2  36356  lindsenlbs  36472  matunitlindflem2  36474  fdc  36602  isbnd3b  36642  ablo4pnp  36737  crngm4  36860  isidlc  36872  pridl  36894  ispridl2  36895  ispridlc  36927  ts3an1  37007  ts3an2  37008  ts3an3  37009  brres2  37125  disjressuc2  37247  xrninxp  37251  dfeqvrels2  37447  dfeqvrel2  37449  dfeqvrel3  37450  dfeldisj3  37578  islshpsm  37839  islshpat  37876  cmtfvalN  38069  cmtvalN  38070  ishlat1  38211  ishlat2  38212  3dim0  38317  2dim  38330  islvol5  38439  lhpexle3  38872  cdleme0ex2N  39084  cdleme0nex  39150  cdlemg2cex  39451  cdlemg33b0  39561  cdlemg33b  39567  cdlemg33c  39568  cdlemg33e  39570  dib1dim  40025  diblsmopel  40031  dihopelvalcpre  40108  lcfls1c  40396  sn-sup2  41339  3anrabdioph  41506  fgraphxp  41939  omge2  42034  faosnf0.11b  42164  dfsucon  42260  pren2  42290  dfrtrcl5  42366  brfvrcld2  42429  df3an2  42506  dfvd3  43338  3impexpVD  43603  rfcnnnub  43706  stoweidlem35  44738  smflimlem4  45477  ndmaovass  45901  nltle2tri  46008  elfz2z  46010  prproropf1olem0  46157  reuprpr  46178  gboge9  46419  sbgoldbalt  46436  nnsum4primesodd  46451  nnsum4primesoddALTV  46452  bgoldbtbndlem4  46463  bgoldbtbnd  46464  ismhm0  46562  rnglz  46651  rngpropd  46660  rngcsect  46832  rngcinv  46833  rngcsectALTV  46844  rngcinvALTV  46845  ringcsect  46883  ringcinv  46884  ringcsectALTV  46907  ringcinvALTV  46908  islindeps  47088  islindeps2  47118  isldepslvec2  47120  elbigo2  47192  line2ylem  47391  io1ii  47507  catprsc  47587  isthincd2  47612  thincsect  47631