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  1118  3jca  1128  3anbi123i  1155  3pm3.2i  1339  3jaob  1426  3anbi123d  1436  3anim123d  1443  an6  1445  an3andi  1482  an33rean  1483  cadan  1606  19.26-3an  1871  nf3and  1897  nf3an  1900  4exdistr  1961  sb3an  2081  eeeanv  2356  mopick2  2640  r19.26-3  3118  r3al  3203  r3ex  3204  rexlimdvvva  3220  3reeanv  3236  ceqsex3v  3549  ceqsex4v  3550  ceqsex8v  3552  rspc4v  3655  sbc3an  3874  elin3  4229  rexdifpr  4681  raltpg  4723  tpss  4862  opthprneg  4889  dfopif  4894  disjxun  5164  otth2  5503  otthg  5505  oteqex  5519  poirr  5620  po3nr  5623  wefrc  5694  otelxp  5744  rabxp  5748  f1orn  6872  fpropnf1  7304  dff1o6  7311  oprabidw  7479  oprabid  7480  oprabv  7510  ndmovass  7638  elovmpo  7695  elovmporab  7696  elovmporab1w  7697  elovmporab1  7698  elovmpt3rab1  7710  dfwe2  7809  opiota  8100  dfxp3  8102  bropopvvv  8131  poxp2  8184  xpord2pred  8186  xpord3pred  8193  sexp3  8194  oaord  8603  oeeu  8659  nnaord  8675  naddasslem1  8750  swoso  8797  fiint  9394  fiintOLD  9395  funsnfsupp  9461  ttrclselem2  9795  alephval3  10179  ingru  10884  axgroth3  10900  ltrelxr  11351  ltxrlt  11360  wloglei  11822  sup2  12251  rexuz2  12964  ltxr  13178  elixx3g  13420  ixxun  13423  dfrp2  13456  elioo4g  13467  elioopnf  13503  elioomnf  13504  elicopnf  13505  elxrge0  13517  divelunit  13554  elfz2  13574  elfzuzb  13578  uzsplit  13656  fznn0  13676  elfzmlbp  13696  preduz  13707  elfzo2  13719  fzolb2  13723  fzouzsplit  13751  ssfzo12bi  13811  fzind2  13835  hashgt23el  14473  ccatsymb  14630  swrdsbslen  14712  swrdspsleq  14713  swrdccatin2  14777  pfxccatin12lem2  14779  pfxccatin12lem3  14780  pfxccatin12  14781  pfxccat3a  14786  repsdf2  14826  repswsymball  14827  repswsymballbi  14828  repswswrd  14832  s3eq3seq  14988  wrdl3s3  15011  s3sndisj  15016  s3iunsndisj  15017  abs2dif  15381  sinltx  16237  divalglem8  16448  divalglem10  16450  divalgb  16452  bitsval2  16471  divgcdz  16557  rplpwr  16605  cncongr1  16714  pythagtriplem2  16864  pythagtrip  16881  prmgaplem4  17101  isstruct  17199  setsstruct2  17221  imasvscafn  17597  xpscf  17625  mreexmrid  17701  iscatd2  17739  issect  17814  issect2  17815  oppcsect  17839  isfunc  17928  funcpropd  17967  fucsect  18042  fucinv  18043  initoeu2  18083  setcsect  18156  setcinv  18157  issgrpd  18768  ismhm0  18825  issubm2  18839  issubg3  19184  resgrpisgrp  19187  eqgval  19217  eqger  19218  cycsubgcl  19246  isgim  19302  gim0to0  19309  gaorb  19347  gaorber  19348  gastacos  19350  symg2bas  19434  galactghm  19446  pmtr3ncom  19517  ispgp  19634  efgcpbllema  19796  efgcpbllemb  19797  eqgabl  19876  qusecsub  19877  cygabl  19933  dprdw  20054  rnglz  20192  rngpropd  20201  ringpropd  20311  ringrghm  20336  isirred2  20447  rngcsect  20658  rngcinv  20659  ringcsect  20692  ringcinv  20693  drngid2  20774  issdrg2  20818  islss  20955  islmim  21084  lmhmpropd  21095  zndvds  21591  znleval  21596  znleval2  21597  obselocv  21771  mpfrcl  22132  matinvgcell  22462  mat1dimscm  22502  scmatscm  22540  scmatf1  22558  mdetunilem7  22645  cpmatacl  22743  cpmatmcl  22746  mat2pmatf1  22756  mat2pmatghm  22757  mat2pmatmul  22758  mat2pmatlin  22762  mat2pmatscmxcl  22767  m2pmfzgsumcl  22775  decpmataa0  22795  monmatcollpw  22806  pmatcollpwscmatlem1  22816  pmatcollpwscmatlem2  22817  pm2mpghm  22843  pm2mpmhmlem2  22846  monmat2matmon  22851  chfacfisf  22881  chfacfisfcpmat  22882  chfacfpmmulgsum2  22892  isbasis3g  22977  leordtvallem2  23240  lmfval  23261  lmbr  23287  lmbr2  23288  lmmo  23409  dfconn2  23448  ptbasin  23606  ptbasfi  23610  txcnpi  23637  ptcnp  23651  hausdiag  23674  qtophmeo  23846  fbunfip  23898  elflim2  23993  hausflimi  24009  isfcls  24038  isfcls2  24042  istmd  24103  istgp  24106  istrg  24193  istdrg  24195  istdrg2  24207  istlm  24214  imasdsf1olem  24404  xmeterval  24463  xmeter  24464  prdsxmslem2  24563  blval2  24596  isngp  24630  isngp2  24631  isngp3  24632  isnlm  24717  cnbl0  24815  cnblcld  24816  elii1  24983  isphtpc  25045  phtpcer  25046  isclmp  25149  iscph  25223  lmmbr  25311  lmmbr2  25312  lmmbrf  25315  iscfil2  25319  iscau3  25331  iscau4  25332  iscauf  25333  caucfil  25336  isbn  25391  ishl2  25423  ovolfcl  25520  ioombl1lem4  25615  mbfmax  25703  iblpos  25848  limcrcl  25929  ig1pval3  26237  ulmdvlem3  26463  ellogdm  26699  relogbcl  26834  fsumvma2  27276  chpchtsum  27281  chpub  27282  dchrelbas3  27300  gausslemma2dlem1a  27427  noetalem1  27804  eqscut  27868  eqscut2  27869  lnhl  28641  colopp  28795  dfcgra2  28856  axeuclidlem  28995  axeuclid  28996  edgupgr  29169  umgr2edg1  29246  subusgr  29324  nbgrel  29375  nb3grpr2  29418  nb3gr2nb  29419  isuvtx  29430  nbupgruvtxres  29442  iscplgredg  29452  cplgr3v  29470  rusgrpropedg  29620  rgrusgrprc  29625  rusgrprc  29626  upgriswlk  29677  wlkonprop  29694  wksonproplem  29740  wksonproplemOLD  29741  usgr2pth0  29801  isclwlke  29813  crctcshtrl  29856  iswwlksnx  29873  wwlknbp  29875  2trld  29971  rusgrnumwwlkl1  30001  rusgrnumwwlkb0  30004  rusgrnumwwlk  30008  clwlkclwwlkflem  30036  erclwwlkref  30052  clwwlkwwlksb  30086  erclwwlknref  30101  clwwlknon2x  30135  0wlk  30148  3spthd  30208  umgr3v3e3cycl  30216  frgr3v  30307  1to3vfriswmgr  30312  frgr2wwlkeu  30359  numclwwlk1lem2fo  30390  dlwwlknondlwlknonf1o  30397  nvex  30643  isnv  30644  dfadj2  31917  cnvadj  31924  adjeq  31967  eleigvec  31989  eleigvec2  31990  chirredi  32426  or3di  32488  eliccelico  32782  omndmul2  33062  pmtrprfv2  33081  fzto1st  33096  psgnfzto1st  33098  isorng  33294  qusker  33342  qusxpid  33356  lsmsnorb  33384  prmidl0  33443  mxidlirred  33465  ply1degltel  33580  ply1degleel  33581  eulerpartlemv  34329  eulerpartlemd  34331  eulerpartlemn  34346  prob01  34378  probun  34384  bnj170  34674  bnj248  34676  bnj252  34679  bnj253  34680  bnj945  34749  bnj1098  34759  bnj1224  34777  bnj150  34852  bnj153  34856  bnj545  34871  bnj557  34877  bnj571  34882  bnj594  34888  bnj864  34898  bnj865  34899  bnj849  34901  bnj964  34919  bnj986  34931  bnj996  34932  bnj1033  34945  bnj1110  34958  bnj1128  34966  bnj1174  34979  subgrwlk  35100  cusgr3cyclex  35104  loop1cycl  35105  2cycl2d  35107  pconnconn  35199  resconn  35214  iscvm  35227  cvmlift2lem12  35282  cvmlift3lem5  35291  satfdm  35337  elmpst  35504  mpstrcl  35509  lediv2aALT  35645  3jcadALT  35655  dfso3  35682  br6  35719  elfuns  35879  brimg  35901  brsuccf  35905  cgrxfr  36019  segcon2  36069  seglecgr12im  36074  seglecgr12  36075  segletr  36078  btwnoutside  36089  broutsideof3  36090  outsideoftr  36093  outsidele  36096  bj-imn3ani  36553  relowlpssretop  37330  wl-df3-3mintru2  37452  lindsenlbs  37575  matunitlindflem2  37577  fdc  37705  isbnd3b  37745  ablo4pnp  37840  crngm4  37963  isidlc  37975  pridl  37997  ispridl2  37998  ispridlc  38030  ts3an1  38110  ts3an2  38111  ts3an3  38112  brres2  38224  disjressuc2  38344  xrninxp  38348  dfeqvrels2  38544  dfeqvrel2  38546  dfeqvrel3  38547  dfeldisj3  38675  islshpsm  38936  islshpat  38973  cmtfvalN  39166  cmtvalN  39167  ishlat1  39308  ishlat2  39309  3dim0  39414  2dim  39427  islvol5  39536  lhpexle3  39969  cdleme0ex2N  40181  cdleme0nex  40247  cdlemg2cex  40548  cdlemg33b0  40658  cdlemg33b  40664  cdlemg33c  40665  cdlemg33e  40667  dib1dim  41122  diblsmopel  41128  dihopelvalcpre  41205  lcfls1c  41493  aks6d1c1p1  42064  aks6d1c1p1rcl  42065  sn-sup2  42447  sn-isghm  42628  3anrabdioph  42738  fgraphxp  43165  omge2  43260  faosnf0.11b  43389  dfsucon  43485  pren2  43515  dfrtrcl5  43591  brfvrcld2  43654  df3an2  43731  dfvd3  44562  3impexpVD  44827  rfcnnnub  44936  stoweidlem35  45956  smflimlem4  46695  ndmaovass  47121  nltle2tri  47228  elfz2z  47230  prproropf1olem0  47376  reuprpr  47397  gboge9  47638  sbgoldbalt  47655  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  bgoldbtbndlem4  47682  bgoldbtbnd  47683  dfvopnbgr2  47725  grlimprop2  47810  uhgrimgrlim  47811  rngcsectALTV  47998  rngcinvALTV  47999  ringcsectALTV  48032  ringcinvALTV  48033  islindeps  48182  islindeps2  48212  isldepslvec2  48214  elbigo2  48286  line2ylem  48485  io1ii  48600  catprsc  48680  isthincd2  48705  thincsect  48724