Definition df-3an 1103

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 473. (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 1101	. 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒)
5	1, 2	wa 400	. . 3 wff (𝜑 ∧ 𝜓)
6	5, 3	wa 400	. 2 wff ((𝜑 ∧ 𝜓) ∧ 𝜒)
7	4, 6	wb 209	1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))

This definition is referenced by:  3anass  1109  3anan32OLD  1112  3ancomb  1114  3anidm  1119  3an4anass  1120  3ioran  1121  3ianor  1122  3impa  1125  3expa  1134  3jca  1144  3anbi123i  1171  3pm3.2i  1356  3jaob  1451  3anbi123d  1462  3anim123d  1469  an6  1472  an3andi  1511  an33rean  1512  cadan  1637  19.26-3an  1900  nf3and  1926  nf3an  1929  4exdistr  1989  sb3an  2113  eeeanv  2380  mopick2  2663  r19.26-3  3124  r3al  3201  r3ex  3202  rexlimdvvva  3221  3reeanv  3236  ceqsex3v  3505  ceqsex4v  3506  ceqsex8v  3508  rspc4v  3600  sbc3an  3807  elin3  4158  rexdifpr  4624  raltpg  4663  tpss  4801  opthprneg  4829  dfopif  4834  disjxun  5106  otth2  5465  otthg  5467  oteqex  5483  poirr  5581  po3nr  5584  wefrc  5655  otelxp  5705  rabxp  5709  f1orn  6831  2f1fvneq  7258  fpropnf1  7265  dff1o6  7273  oprabidw  7441  oprabid  7442  oprabv  7470  ndmovass  7598  elovmpo  7655  elovmporab  7656  elovmporab1w  7657  elovmporab1  7658  elovmpt3rab1  7670  dfwe2  7772  opiota  8055  dfxp3  8057  bropopvvv  8084  poxp2  8138  xpord2pred  8140  xpord3pred  8147  sexp3  8148  oaord  8531  oeeu  8588  nnaord  8604  naddasslem1  8680  swoso  8728  fiint  9285  funsnfsupp  9351  ttrclselem2  9694  alephval3  10093  ingru  10799  axgroth3  10815  ltrelxr  11269  ltxrlt  11279  wloglei  11745  sup2  12170  rexuz2  12922  ltxr  13139  elixx3g  13384  ixxun  13387  dfrp2  13420  elioo4g  13432  elioopnf  13469  elioomnf  13470  elicopnf  13471  elxrge0  13483  divelunit  13520  elfz2  13541  elfzuzb  13545  uzsplit  13623  fznn0  13646  elfzmlbp  13666  preduz  13677  elfzo2  13689  fzolb2  13694  fzouzsplit  13722  ssfzo12bi  13789  fzind2  13816  hashgt23el  14460  ccatsymb  14619  swrdsbslen  14701  swrdspsleq  14702  swrdccatin2  14765  pfxccatin12lem2  14767  pfxccatin12lem3  14768  pfxccatin12  14769  pfxccat3a  14774  repsdf2  14814  repswsymball  14815  repswsymballbi  14816  repswswrd  14820  s3eq3seq  14975  wrdl3s3  14998  s3sndisj  15003  s3iunsndisj  15004  abs2dif  15383  sinltx  16244  divalglem8  16457  divalglem10  16459  divalgb  16461  bitsval2  16482  divgcdz  16568  rplpwr  16615  cncongr1  16724  pythagtriplem2  16876  pythagtrip  16893  prmgaplem4  17113  isstruct  17211  setsstruct2  17233  imasvscafn  17590  xpscf  17618  mreexmrid  17698  iscatd2  17736  issect  17809  issect2  17810  oppcsect  17834  isfunc  17920  funcpropd  17958  fucsect  18031  fucinv  18032  initoeu2  18072  setcsect  18145  setcinv  18146  issgrpd  18787  ismhm0  18847  issubm2  18861  issubg3  19210  resgrpisgrp  19213  eqgval  19244  eqger  19245  qusxpid  19250  cycsubgcl  19276  isgim  19331  gim0to0  19338  gaorb  19376  gaorber  19377  gastacos  19379  symg2bas  19462  galactghm  19473  pmtr3ncom  19544  ispgp  19661  efgcpbllema  19823  efgcpbllemb  19824  eqgabl  19903  qusecsub  19904  cygabl  19960  dprdw  20081  omndmul2  20202  rnglz  20242  rngpropd  20251  ringpropd  20370  ringrghm  20395  isirred2  20502  rngcsect  20720  rngcinv  20721  ringcsect  20754  ringcinv  20755  drngid2  20836  issdrg2  20877  isorng  20943  islss  21034  islmim  21162  lmhmpropd  21173  prmidl0  21457  zndvds  21678  znleval  21683  znleval2  21684  obselocv  21857  mpfrcl  22215  matinvgcell  22571  mat1dimscm  22611  scmatscm  22649  scmatf1  22667  mdetunilem7  22754  cpmatacl  22852  cpmatmcl  22855  mat2pmatf1  22865  mat2pmatghm  22866  mat2pmatmul  22867  mat2pmatlin  22871  mat2pmatscmxcl  22876  m2pmfzgsumcl  22884  decpmataa0  22904  monmatcollpw  22915  pmatcollpwscmatlem1  22925  pmatcollpwscmatlem2  22926  pm2mpghm  22952  pm2mpmhmlem2  22955  monmat2matmon  22960  chfacfisf  22990  chfacfisfcpmat  22991  chfacfpmmulgsum2  23001  isbasis3g  23085  leordtvallem2  23347  lmfval  23368  lmbr  23394  lmbr2  23395  lmmo  23516  dfconn2  23555  ptbasin  23713  ptbasfi  23717  txcnpi  23744  ptcnp  23758  hausdiag  23781  qtophmeo  23953  fbunfip  24005  elflim2  24100  hausflimi  24116  isfcls  24145  isfcls2  24149  istmd  24210  istgp  24213  istrg  24300  istdrg  24302  istdrg2  24314  istlm  24321  imasdsf1olem  24509  xmeterval  24568  xmeter  24569  prdsxmslem2  24665  blval2  24698  isngp  24732  isngp2  24733  isngp3  24734  isnlm  24811  cnbl0  24909  cnblcld  24910  elii1  25073  isphtpc  25132  phtpcer  25133  isclmp  25235  iscph  25308  lmmbr  25396  lmmbr2  25397  lmmbrf  25400  iscfil2  25404  iscau3  25416  iscau4  25417  iscauf  25418  caucfil  25421  isbn  25476  ishl2  25508  ovolfcl  25604  ioombl1lem4  25699  mbfmax  25787  iblpos  25931  limcrcl  26012  ig1pval3  26314  ulmdvlem3  26541  ellogdm  26780  relogbcl  26914  fsumvma2  27354  chpchtsum  27359  chpub  27360  dchrelbas3  27378  gausslemma2dlem1a  27505  noetalem1  27881  sltssnb  27938  eqcuts  27954  eqcuts2  27955  lnhl  28863  colopp  29026  dfcgra2  29114  axeuclidlem  29278  axeuclid  29279  edgupgr  29450  umgr2edg1  29527  subusgr  29605  nbgrel  29656  nb3grpr2  29699  nb3gr2nb  29700  isuvtx  29711  nbupgruvtxres  29723  iscplgredg  29733  cplgr3v  29751  rusgrpropedg  29900  rgrusgrprc  29905  rusgrprc  29906  upgriswlk  29956  wlkonprop  29972  wksonproplem  30018  usgr2pth0  30080  isclwlke  30092  crctcshtrl  30138  iswwlksnx  30155  wwlknbp  30157  2trld  30253  rusgrnumwwlkl1  30286  rusgrnumwwlkb0  30289  rusgrnumwwlk  30293  clwlkclwwlkflem  30321  erclwwlkref  30337  clwwlkwwlksb  30371  erclwwlknref  30386  clwwlknon2x  30420  0wlk  30433  3spthd  30493  umgr3v3e3cycl  30501  frgr3v  30592  1to3vfriswmgr  30597  frgr2wwlkeu  30644  numclwwlk1lem2fo  30675  dlwwlknondlwlknonf1o  30682  nvex  30929  isnv  30930  dfadj2  32203  cnvadj  32210  adjeq  32253  eleigvec  32275  eleigvec2  32276  chirredi  32712  or3di  32773  tpssg  32849  eliccelico  33088  pmtrprfv2  33374  fzto1st  33389  psgnfzto1st  33391  qusker  33635  lsmsnorb  33670  mxidlirred  33721  ply1degltel  33850  ply1degleel  33851  eulerpartlemv  34720  eulerpartlemd  34722  eulerpartlemn  34737  prob01  34769  probun  34775  bnj170  35053  bnj248  35055  bnj252  35058  bnj253  35059  bnj945  35128  bnj1098  35138  bnj1224  35155  bnj150  35230  bnj153  35234  bnj545  35249  bnj557  35255  bnj571  35260  bnj594  35266  bnj864  35276  bnj865  35277  bnj849  35279  bnj964  35297  bnj986  35309  bnj996  35310  bnj1033  35323  bnj1110  35336  bnj1128  35344  bnj1174  35357  subgrwlk  35578  cusgr3cyclex  35582  loop1cycl  35583  2cycl2d  35585  pconnconn  35677  resconn  35692  iscvm  35705  cvmlift2lem12  35760  cvmlift3lem5  35769  satfdm  35815  elmpst  35982  mpstrcl  35987  lediv2aALT  36123  3jcadALT  36133  dfso3  36166  br6  36203  elfuns  36359  brimg  36381  lemsuccf  36385  cgrxfr  36501  segcon2  36551  seglecgr12im  36556  seglecgr12  36557  segletr  36560  btwnoutside  36571  broutsideof3  36572  outsideoftr  36575  outsidele  36578  bj-imn3ani  37124  relowlpssretop  37954  wl-df3-3mintru2  38076  lindsenlbs  38210  matunitlindflem2  38212  fdc  38340  isbnd3b  38380  ablo4pnp  38475  crngm4  38598  isidlc  38610  pridl  38632  ispridl2  38633  ispridlc  38665  ts3an1  38745  ts3an2  38746  ts3an3  38747  brres2  38868  disjressuc2  39006  xrninxp  39010  dfsuccl4  39069  dfeqvrels2  39267  dfeqvrel2  39269  dfeqvrel3  39270  dfeldisj3  39406  islshpsm  39700  islshpat  39737  cmtfvalN  39930  cmtvalN  39931  ishlat1  40072  ishlat2  40073  3dim0  40177  2dim  40190  islvol5  40299  lhpexle3  40732  cdleme0ex2N  40944  cdleme0nex  41010  cdlemg2cex  41311  cdlemg33b0  41421  cdlemg33b  41427  cdlemg33c  41428  cdlemg33e  41430  dib1dim  41885  diblsmopel  41891  dihopelvalcpre  41968  lcfls1c  42256  aks6d1c1p1  42820  aks6d1c1p1rcl  42821  sn-sup2  43211  sn-isghm  43353  3anrabdioph  43461  fgraphxp  43879  omge2  43973  faosnf0.11b  44101  dfsucon  44197  pren2  44227  dfrtrcl5  44303  brfvrcld2  44366  df3an2  44443  dfvd3  45248  3impexpVD  45512  modelaxreplem1  45635  rfcnnnub  45704  stoweidlem35  46697  smflimlem4  47436  ndmaovass  47888  nltle2tri  47995  elfz2z  47997  prproropf1olem0  48196  reuprpr  48217  gboge9  48474  sbgoldbalt  48491  nnsum4primesodd  48506  nnsum4primesoddALTV  48507  bgoldbtbndlem4  48518  bgoldbtbnd  48519  dfvopnbgr2  48563  isuspgrim  48606  isubgr3stgrlem7  48682  grlimprop2  48696  uhgrimgrlim  48697  pgn4cyclex  48836  rngcsectALTV  48985  rngcinvALTV  48986  ringcsectALTV  49019  ringcinvALTV  49020  islindeps  49178  islindeps2  49208  isldepslvec2  49210  elbigo2  49277  line2ylem  49476  io1ii  49644  catprsc  49736  0funcglem  49806  0funclem  49809  catcsect  50121  isthincd2  50160  thincsect  50190  2arwcatlem1  50318