Definition df-3an 1088

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 1086	. 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  1094  3anan32  1096  3ancomb  1098  3anidm  1103  3an4anass  1104  3ioran  1105  3ianor  1106  3impa  1109  3expa  1117  3jca  1127  3anbi123i  1154  3pm3.2i  1338  3jaob  1425  3anbi123d  1435  3anim123d  1442  an6  1444  an3andi  1481  an33rean  1482  cadan  1605  19.26-3an  1869  nf3and  1895  nf3an  1898  4exdistr  1958  sb3an  2078  eeeanv  2350  mopick2  2634  r19.26-3  3109  r3al  3194  r3ex  3195  rexlimdvvva  3211  3reeanv  3227  ceqsex3v  3536  ceqsex4v  3537  ceqsex8v  3539  rspc4v  3641  sbc3an  3860  elin3  4215  rexdifpr  4663  raltpg  4702  tpss  4841  opthprneg  4869  dfopif  4874  disjxun  5145  otth2  5493  otthg  5495  oteqex  5509  poirr  5608  po3nr  5611  wefrc  5682  otelxp  5732  rabxp  5736  f1orn  6858  fpropnf1  7286  dff1o6  7294  oprabidw  7461  oprabid  7462  oprabv  7492  ndmovass  7620  elovmpo  7677  elovmporab  7678  elovmporab1w  7679  elovmporab1  7680  elovmpt3rab1  7692  dfwe2  7792  opiota  8082  dfxp3  8084  bropopvvv  8113  poxp2  8166  xpord2pred  8168  xpord3pred  8175  sexp3  8176  oaord  8583  oeeu  8639  nnaord  8655  naddasslem1  8730  swoso  8777  fiint  9363  fiintOLD  9364  funsnfsupp  9429  ttrclselem2  9763  alephval3  10147  ingru  10852  axgroth3  10868  ltrelxr  11319  ltxrlt  11328  wloglei  11792  sup2  12221  rexuz2  12938  ltxr  13154  elixx3g  13396  ixxun  13399  dfrp2  13432  elioo4g  13443  elioopnf  13479  elioomnf  13480  elicopnf  13481  elxrge0  13493  divelunit  13530  elfz2  13550  elfzuzb  13554  uzsplit  13632  fznn0  13655  elfzmlbp  13675  preduz  13686  elfzo2  13698  fzolb2  13702  fzouzsplit  13730  ssfzo12bi  13796  fzind2  13820  hashgt23el  14459  ccatsymb  14616  swrdsbslen  14698  swrdspsleq  14699  swrdccatin2  14763  pfxccatin12lem2  14765  pfxccatin12lem3  14766  pfxccatin12  14767  pfxccat3a  14772  repsdf2  14812  repswsymball  14813  repswsymballbi  14814  repswswrd  14818  s3eq3seq  14974  wrdl3s3  14997  s3sndisj  15002  s3iunsndisj  15003  abs2dif  15367  sinltx  16221  divalglem8  16433  divalglem10  16435  divalgb  16437  bitsval2  16458  divgcdz  16544  rplpwr  16591  cncongr1  16700  pythagtriplem2  16850  pythagtrip  16867  prmgaplem4  17087  isstruct  17185  setsstruct2  17207  imasvscafn  17583  xpscf  17611  mreexmrid  17687  iscatd2  17725  issect  17800  issect2  17801  oppcsect  17825  isfunc  17914  funcpropd  17953  fucsect  18028  fucinv  18029  initoeu2  18069  setcsect  18142  setcinv  18143  issgrpd  18755  ismhm0  18815  issubm2  18829  issubg3  19174  resgrpisgrp  19177  eqgval  19207  eqger  19208  cycsubgcl  19236  isgim  19292  gim0to0  19299  gaorb  19337  gaorber  19338  gastacos  19340  symg2bas  19424  galactghm  19436  pmtr3ncom  19507  ispgp  19624  efgcpbllema  19786  efgcpbllemb  19787  eqgabl  19866  qusecsub  19867  cygabl  19923  dprdw  20044  rnglz  20182  rngpropd  20191  ringpropd  20301  ringrghm  20326  isirred2  20437  rngcsect  20652  rngcinv  20653  ringcsect  20686  ringcinv  20687  drngid2  20768  issdrg2  20812  islss  20949  islmim  21078  lmhmpropd  21089  zndvds  21585  znleval  21590  znleval2  21591  obselocv  21765  mpfrcl  22126  matinvgcell  22456  mat1dimscm  22496  scmatscm  22534  scmatf1  22552  mdetunilem7  22639  cpmatacl  22737  cpmatmcl  22740  mat2pmatf1  22750  mat2pmatghm  22751  mat2pmatmul  22752  mat2pmatlin  22756  mat2pmatscmxcl  22761  m2pmfzgsumcl  22769  decpmataa0  22789  monmatcollpw  22800  pmatcollpwscmatlem1  22810  pmatcollpwscmatlem2  22811  pm2mpghm  22837  pm2mpmhmlem2  22840  monmat2matmon  22845  chfacfisf  22875  chfacfisfcpmat  22876  chfacfpmmulgsum2  22886  isbasis3g  22971  leordtvallem2  23234  lmfval  23255  lmbr  23281  lmbr2  23282  lmmo  23403  dfconn2  23442  ptbasin  23600  ptbasfi  23604  txcnpi  23631  ptcnp  23645  hausdiag  23668  qtophmeo  23840  fbunfip  23892  elflim2  23987  hausflimi  24003  isfcls  24032  isfcls2  24036  istmd  24097  istgp  24100  istrg  24187  istdrg  24189  istdrg2  24201  istlm  24208  imasdsf1olem  24398  xmeterval  24457  xmeter  24458  prdsxmslem2  24557  blval2  24590  isngp  24624  isngp2  24625  isngp3  24626  isnlm  24711  cnbl0  24809  cnblcld  24810  elii1  24977  isphtpc  25039  phtpcer  25040  isclmp  25143  iscph  25217  lmmbr  25305  lmmbr2  25306  lmmbrf  25309  iscfil2  25313  iscau3  25325  iscau4  25326  iscauf  25327  caucfil  25330  isbn  25385  ishl2  25417  ovolfcl  25514  ioombl1lem4  25609  mbfmax  25697  iblpos  25842  limcrcl  25923  ig1pval3  26231  ulmdvlem3  26459  ellogdm  26695  relogbcl  26830  fsumvma2  27272  chpchtsum  27277  chpub  27278  dchrelbas3  27296  gausslemma2dlem1a  27423  noetalem1  27800  eqscut  27864  eqscut2  27865  lnhl  28637  colopp  28791  dfcgra2  28852  axeuclidlem  28991  axeuclid  28992  edgupgr  29165  umgr2edg1  29242  subusgr  29320  nbgrel  29371  nb3grpr2  29414  nb3gr2nb  29415  isuvtx  29426  nbupgruvtxres  29438  iscplgredg  29448  cplgr3v  29466  rusgrpropedg  29616  rgrusgrprc  29621  rusgrprc  29622  upgriswlk  29673  wlkonprop  29690  wksonproplem  29736  wksonproplemOLD  29737  usgr2pth0  29797  isclwlke  29809  crctcshtrl  29852  iswwlksnx  29869  wwlknbp  29871  2trld  29967  rusgrnumwwlkl1  29997  rusgrnumwwlkb0  30000  rusgrnumwwlk  30004  clwlkclwwlkflem  30032  erclwwlkref  30048  clwwlkwwlksb  30082  erclwwlknref  30097  clwwlknon2x  30131  0wlk  30144  3spthd  30204  umgr3v3e3cycl  30212  frgr3v  30303  1to3vfriswmgr  30308  frgr2wwlkeu  30355  numclwwlk1lem2fo  30386  dlwwlknondlwlknonf1o  30393  nvex  30639  isnv  30640  dfadj2  31913  cnvadj  31920  adjeq  31963  eleigvec  31985  eleigvec2  31986  chirredi  32422  or3di  32487  eliccelico  32785  omndmul2  33071  pmtrprfv2  33090  fzto1st  33105  psgnfzto1st  33107  isorng  33308  qusker  33356  qusxpid  33370  lsmsnorb  33398  prmidl0  33457  mxidlirred  33479  ply1degltel  33594  ply1degleel  33595  eulerpartlemv  34345  eulerpartlemd  34347  eulerpartlemn  34362  prob01  34394  probun  34400  bnj170  34690  bnj248  34692  bnj252  34695  bnj253  34696  bnj945  34765  bnj1098  34775  bnj1224  34793  bnj150  34868  bnj153  34872  bnj545  34887  bnj557  34893  bnj571  34898  bnj594  34904  bnj864  34914  bnj865  34915  bnj849  34917  bnj964  34935  bnj986  34947  bnj996  34948  bnj1033  34961  bnj1110  34974  bnj1128  34982  bnj1174  34995  subgrwlk  35116  cusgr3cyclex  35120  loop1cycl  35121  2cycl2d  35123  pconnconn  35215  resconn  35230  iscvm  35243  cvmlift2lem12  35298  cvmlift3lem5  35307  satfdm  35353  elmpst  35520  mpstrcl  35525  lediv2aALT  35661  3jcadALT  35671  dfso3  35699  br6  35736  elfuns  35896  brimg  35918  brsuccf  35922  cgrxfr  36036  segcon2  36086  seglecgr12im  36091  seglecgr12  36092  segletr  36095  btwnoutside  36106  broutsideof3  36107  outsideoftr  36110  outsidele  36113  bj-imn3ani  36569  relowlpssretop  37346  wl-df3-3mintru2  37468  lindsenlbs  37601  matunitlindflem2  37603  fdc  37731  isbnd3b  37771  ablo4pnp  37866  crngm4  37989  isidlc  38001  pridl  38023  ispridl2  38024  ispridlc  38056  ts3an1  38136  ts3an2  38137  ts3an3  38138  brres2  38249  disjressuc2  38369  xrninxp  38373  dfeqvrels2  38569  dfeqvrel2  38571  dfeqvrel3  38572  dfeldisj3  38700  islshpsm  38961  islshpat  38998  cmtfvalN  39191  cmtvalN  39192  ishlat1  39333  ishlat2  39334  3dim0  39439  2dim  39452  islvol5  39561  lhpexle3  39994  cdleme0ex2N  40206  cdleme0nex  40272  cdlemg2cex  40573  cdlemg33b0  40683  cdlemg33b  40689  cdlemg33c  40690  cdlemg33e  40692  dib1dim  41147  diblsmopel  41153  dihopelvalcpre  41230  lcfls1c  41518  aks6d1c1p1  42088  aks6d1c1p1rcl  42089  sn-sup2  42477  sn-isghm  42659  3anrabdioph  42769  fgraphxp  43192  omge2  43287  faosnf0.11b  43416  dfsucon  43512  pren2  43542  dfrtrcl5  43618  brfvrcld2  43681  df3an2  43758  dfvd3  44588  3impexpVD  44853  modelaxreplem1  44942  rfcnnnub  44973  stoweidlem35  45990  smflimlem4  46729  ndmaovass  47155  nltle2tri  47262  elfz2z  47264  prproropf1olem0  47426  reuprpr  47447  gboge9  47688  sbgoldbalt  47705  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  bgoldbtbndlem4  47732  bgoldbtbnd  47733  dfvopnbgr2  47776  isubgr3stgrlem7  47874  grlimprop2  47888  uhgrimgrlim  47889  rngcsectALTV  48118  rngcinvALTV  48119  ringcsectALTV  48152  ringcinvALTV  48153  islindeps  48298  islindeps2  48328  isldepslvec2  48330  elbigo2  48401  line2ylem  48600  io1ii  48716  catprsc  48801  isthincd2  48837  thincsect  48857