Definition df-3an 1105

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

This definition is used by:  3anass  1111  3anan32OLD  1114  3ancomb  1116  3anidm  1121  3an4anass  1122  3ioran  1123  3ianor  1124  3impa  1127  3expa  1136  3jca  1146  3anbi123i  1173  3pm3.2i  1358  3jaob  1453  3anbi123d  1464  3anim123d  1471  an6  1474  an3andi  1513  an33rean  1514  cadan  1642  19.26-3an  1905  nf3and  1931  nf3an  1934  4exdistr  1994  sb3an  2118  eeeanv  2381  mopick2  2664  r19.26-3  3125  r3al  3202  r3ex  3203  rexlimdvvva  3222  3reeanv  3237  ceqsex3v  3505  ceqsex4v  3506  ceqsex8v  3508  rspc4v  3599  sbc3an  3806  elin3  4155  rexdifpr  4623  raltpg  4662  tpss  4800  opthprneg  4828  dfopif  4833  disjxun  5105  otth2  5463  otthg  5465  oteqex  5481  poirr  5579  po3nr  5582  wefrc  5653  otelxp  5703  rabxp  5707  f1orn  6832  2f1fvneq  7260  fpropnf1  7267  dff1o6  7279  oprabidw  7447  oprabid  7448  oprabv  7476  ndmovass  7605  elovmpo  7662  elovmporab  7663  elovmporab1w  7664  elovmporab1  7665  elovmpt3rab1  7677  dfwe2  7776  opiota  8059  dfxp3  8061  bropopvvv  8090  poxp2  8144  xpord2pred  8146  xpord3pred  8153  sexp3  8154  oaord  8537  oeeu  8594  nnaord  8610  naddasslem1  8686  swoso  8734  fiint  9299  funsnfsupp  9365  ttrclselem2  9708  alephval3  10116  ingru  10827  axgroth3  10843  ltrelxr  11297  ltxrlt  11307  wloglei  11773  sup2  12198  rexuz2  12951  ltxr  13168  elixx3g  13413  ixxun  13416  dfrp2  13449  elioo4g  13461  elioopnf  13498  elioomnf  13499  elicopnf  13500  elxrge0  13512  divelunit  13549  elfz2  13570  elfzuzb  13574  uzsplit  13653  fznn0  13676  elfzmlbp  13696  preduz  13707  elfzo2  13719  fzolb2  13724  fzouzsplit  13752  ssfzo12bi  13819  fzind2  13846  hashgt23el  14491  ccatsymb  14650  swrdsbslen  14736  swrdspsleq  14737  swrdccatin2  14800  pfxccatin12lem2  14802  pfxccatin12lem3  14803  pfxccatin12  14804  pfxccat3a  14809  repsdf2  14851  repswsymball  14852  repswsymballbi  14853  repswswrd  14857  s3eq3seq  15012  wrdl3s3  15037  s3sndisj  15042  s3iunsndisj  15043  abs2dif  15422  sinltx  16281  divalglem8  16494  divalglem10  16496  divalgb  16498  bitsval2  16519  divgcdz  16605  rplpwr  16652  cncongr1  16761  pythagtriplem2  16913  pythagtrip  16930  prmgaplem4  17150  isstruct  17248  setsstruct2  17270  imasvscafn  17627  xpscf  17655  mreexmrid  17735  iscatd2  17773  issect  17846  issect2  17847  oppcsect  17871  isfunc  17957  funcpropd  17995  fucsect  18068  fucinv  18069  initoeu2  18109  setcsect  18182  setcinv  18183  issgrpd  18834  ismhm0  18899  issubm2  18913  issubg3  19269  resgrpisgrp  19272  eqgval  19303  eqger  19304  qusxpid  19309  cycsubgcl  19335  isgim  19390  gim0to0  19397  gaorb  19435  gaorber  19436  gastacos  19438  symg2bas  19521  galactghm  19532  pmtr3ncom  19603  ispgp  19720  efgcpbllema  19882  efgcpbllemb  19883  eqgabl  19962  qusecsub  19963  cygabl  20019  dprdw  20140  omndmul2  20261  rnglz  20301  rngpropd  20310  ringpropd  20431  ringrghm  20456  isirred2  20563  rngcsect  20799  rngcinv  20800  ringcsect  20833  ringcinv  20834  isdrng5  20918  drngid2  20920  issdrg2  20962  isorng  21028  islss  21119  islmim  21247  lmhmpropd  21258  prmidl0  21542  zndvds  21763  znleval  21768  znleval2  21769  obselocv  21942  lindsenlbs  22065  mpfrcl  22302  matinvgcell  22658  mat1dimscm  22698  scmatscm  22736  scmatf1  22754  mdetunilem7  22841  matunitlindflem2  22903  cpmatacl  22942  cpmatmcl  22945  mat2pmatf1  22955  mat2pmatghm  22956  mat2pmatmul  22957  mat2pmatlin  22961  mat2pmatscmxcl  22966  m2pmfzgsumcl  22974  decpmataa0  22994  monmatcollpw  23005  pmatcollpwscmatlem1  23015  pmatcollpwscmatlem2  23016  pm2mpghm  23042  pm2mpmhmlem2  23045  monmat2matmon  23050  chfacfisf  23080  chfacfisfcpmat  23081  chfacfpmmulgsum2  23091  isbasis3g  23175  leordtvallem2  23437  lmfval  23458  lmbr  23484  lmbr2  23485  lmmo  23606  dfconn2  23645  ptbasin  23804  ptbasfi  23808  txcnpi  23835  ptcnp  23849  hausdiag  23872  qtophmeo  24044  fbunfip  24096  elflim2  24191  hausflimi  24207  isfcls  24236  isfcls2  24240  istmd  24301  istgp  24304  istrg  24391  istdrg  24393  istdrg2  24405  istlm  24412  imasdsf1olem  24600  xmeterval  24659  xmeter  24660  prdsxmslem2  24756  blval2  24789  isngp  24823  isngp2  24824  isngp3  24825  isnlm  24902  cnbl0  25000  cnblcld  25001  elii1  25164  isphtpc  25223  phtpcer  25224  isclmp  25326  iscph  25399  lmmbr  25487  lmmbr2  25488  lmmbrf  25491  iscfil2  25495  iscau3  25507  iscau4  25508  iscauf  25509  caucfil  25512  isbn  25567  ishl2  25599  ovolfcl  25695  ioombl1lem4  25790  mbfmax  25878  iblpos  26022  limcrcl  26103  ig1pval3  26405  ulmdvlem3  26635  ellogdm  26874  relogbcl  27008  fsumvma2  27448  chpchtsum  27453  chpub  27454  dchrelbas3  27472  gausslemma2dlem1a  27599  noetalem1  27975  sltssnb  28032  eqcuts  28048  eqcuts2  28049  lnhl  28958  colopp  29124  dfcgra2  29215  axeuclidlem  29405  axeuclid  29406  edgupgr  29577  umgr2edg1  29657  subusgr  29735  nbgrel  29786  nb3grpr2  29829  nb3gr2nb  29830  isuvtx  29841  nbupgruvtxres  29853  iscplgredg  29863  cplgr3v  29881  rusgrpropedg  30030  rgrusgrprc  30035  rusgrprc  30036  upgriswlk  30086  wlkonprop  30102  subgrwlk  30134  wksonproplem  30152  usgr2pth0  30216  isclwlke  30229  crctcshtrl  30277  iswwlksnx  30294  wwlknbp  30296  2trld  30392  rusgrnumwwlkl1  30425  rusgrnumwwlkb0  30428  rusgrnumwwlk  30432  clwlkclwwlkflem  30460  erclwwlkref  30476  clwwlkwwlksb  30510  erclwwlknref  30525  clwwlknon2x  30559  0wlk  30572  loop1cycl  30609  3spthd  30642  umgr3v3e3cycl  30650  frgr3v  30741  1to3vfriswmgr  30746  frgr2wwlkeu  30793  numclwwlk1lem2fo  30824  dlwwlknondlwlknonf1o  30831  nvex  31078  isnv  31079  dfadj2  32352  cnvadj  32359  adjeq  32402  eleigvec  32424  eleigvec2  32425  chirredi  32861  or3di  32922  tpssg  32998  eliccelico  33235  pmtrprfv2  33515  fzto1st  33530  psgnfzto1st  33532  qusker  33776  lsmsnorb  33811  mxidlirred  33862  ply1degltel  33991  ply1degleel  33992  eulerpartlemv  34862  eulerpartlemd  34864  eulerpartlemn  34879  prob01  34911  probun  34917  bnj170  35195  bnj248  35197  bnj252  35200  bnj253  35201  bnj945  35270  bnj1098  35280  bnj1224  35297  bnj150  35372  bnj153  35376  bnj545  35391  bnj557  35397  bnj571  35402  bnj594  35408  bnj864  35418  bnj865  35419  bnj849  35421  bnj964  35439  bnj986  35451  bnj996  35452  bnj1033  35465  bnj1110  35478  bnj1128  35486  bnj1174  35499  cusgr3cyclex  35712  2cycl2d  35713  pconnconn  35797  resconn  35812  iscvm  35825  cvmlift2lem12  35880  cvmlift3lem5  35889  satfdm  35935  elmpst  36102  mpstrcl  36107  lediv2aALT  36243  3jcadALT  36253  dfso3  36286  br6  36323  elfuns  36479  brimg  36501  lemsuccf  36505  cgrxfr  36622  segcon2  36672  seglecgr12im  36677  seglecgr12  36678  segletr  36681  btwnoutside  36692  broutsideof3  36693  outsideoftr  36696  outsidele  36699  bj-imn3ani  37275  relowlpssretop  38105  wl-df3-3mintru2  38227  fdc  38482  isbnd3b  38522  ablo4pnp  38617  crngm4  38740  isidlc  38752  pridl  38774  ispridl2  38775  ispridlc  38807  ts3an1  38885  ts3an2  38886  ts3an3  38887  brres2  39008  disjressuc2  39146  xrninxp  39150  dfsuccl4  39209  dfeqvrels2  39407  dfeqvrel2  39409  dfeqvrel3  39410  dfeldisj3  39546  islshpsm  39840  islshpat  39877  cmtfvalN  40070  cmtvalN  40071  ishlat1  40212  ishlat2  40213  3dim0  40317  2dim  40330  islvol5  40439  lhpexle3  40872  cdleme0ex2N  41084  cdleme0nex  41150  cdlemg2cex  41451  cdlemg33b0  41561  cdlemg33b  41567  cdlemg33c  41568  cdlemg33e  41570  dib1dim  42025  diblsmopel  42031  dihopelvalcpre  42108  lcfls1c  42396  aks6d1c1p1  42960  aks6d1c1p1rcl  42961  sn-sup2  43366  sn-isghm  43506  3anrabdioph  43614  fgraphxp  44032  omge2  44126  faosnf0.11b  44254  dfsucon  44350  pren2  44380  dfrtrcl5  44456  brfvrcld2  44519  df3an2  44596  dfvd3  45401  3impexpVD  45665  modelaxreplem1  45788  rfcnnnub  45857  stoweidlem35  46850  smflimlem4  47589  ndmaovass  48081  nltle2tri  48188  elfz2z  48190  prproropf1olem0  48389  reuprpr  48410  gboge9  48667  sbgoldbalt  48684  nnsum4primesodd  48699  nnsum4primesoddALTV  48700  bgoldbtbndlem4  48711  bgoldbtbnd  48712  dfvopnbgr2  48756  isuspgrim  48799  isubgr3stgrlem7  48875  grlimprop2  48889  uhgrimgrlim  48890  pgn4cyclex  49029  rngcsectALTV  49177  rngcinvALTV  49178  ringcsectALTV  49211  ringcinvALTV  49212  islindeps  49370  islindeps2  49400  isldepslvec2  49402  elbigo2  49469  line2ylem  49668  io1ii  49834  catprsc  49926  0funcglem  49996  0funclem  49999  catcsect  50311  isthincd2  50350  thincsect  50380  2arwcatlem1  50508