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  1118  3jca  1128  3anbi123i  1155  3pm3.2i  1340  3jaob  1428  3anbi123d  1438  3anim123d  1445  an6  1447  an3andi  1484  an33rean  1485  cadan  1609  19.26-3an  1872  nf3and  1898  nf3an  1901  4exdistr  1961  sb3an  2081  eeeanv  2351  mopick2  2636  r19.26-3  3099  r3al  3182  r3ex  3183  rexlimdvvva  3199  3reeanv  3214  ceqsex3v  3516  ceqsex4v  3517  ceqsex8v  3519  rspc4v  3621  sbc3an  3830  elin3  4181  rexdifpr  4635  raltpg  4674  tpss  4813  opthprneg  4841  dfopif  4846  disjxun  5117  otth2  5458  otthg  5460  oteqex  5475  poirr  5573  po3nr  5576  wefrc  5648  otelxp  5698  rabxp  5702  f1orn  6827  2f1fvneq  7252  fpropnf1  7259  dff1o6  7267  oprabidw  7434  oprabid  7435  oprabv  7465  ndmovass  7593  elovmpo  7650  elovmporab  7651  elovmporab1w  7652  elovmporab1  7653  elovmpt3rab1  7665  dfwe2  7766  opiota  8056  dfxp3  8058  bropopvvv  8087  poxp2  8140  xpord2pred  8142  xpord3pred  8149  sexp3  8150  oaord  8557  oeeu  8613  nnaord  8629  naddasslem1  8704  swoso  8751  fiint  9336  fiintOLD  9337  funsnfsupp  9402  ttrclselem2  9738  alephval3  10122  ingru  10827  axgroth3  10843  ltrelxr  11294  ltxrlt  11303  wloglei  11767  sup2  12196  rexuz2  12913  ltxr  13129  elixx3g  13373  ixxun  13376  dfrp2  13409  elioo4g  13421  elioopnf  13458  elioomnf  13459  elicopnf  13460  elxrge0  13472  divelunit  13509  elfz2  13529  elfzuzb  13533  uzsplit  13611  fznn0  13634  elfzmlbp  13654  preduz  13665  elfzo2  13677  fzolb2  13681  fzouzsplit  13709  ssfzo12bi  13775  fzind2  13799  hashgt23el  14440  ccatsymb  14598  swrdsbslen  14680  swrdspsleq  14681  swrdccatin2  14745  pfxccatin12lem2  14747  pfxccatin12lem3  14748  pfxccatin12  14749  pfxccat3a  14754  repsdf2  14794  repswsymball  14795  repswsymballbi  14796  repswswrd  14800  s3eq3seq  14956  wrdl3s3  14979  s3sndisj  14984  s3iunsndisj  14985  abs2dif  15349  sinltx  16205  divalglem8  16417  divalglem10  16419  divalgb  16421  bitsval2  16442  divgcdz  16528  rplpwr  16575  cncongr1  16684  pythagtriplem2  16835  pythagtrip  16852  prmgaplem4  17072  isstruct  17169  setsstruct2  17191  imasvscafn  17549  xpscf  17577  mreexmrid  17653  iscatd2  17691  issect  17764  issect2  17765  oppcsect  17789  isfunc  17875  funcpropd  17913  fucsect  17986  fucinv  17987  initoeu2  18027  setcsect  18100  setcinv  18101  issgrpd  18706  ismhm0  18766  issubm2  18780  issubg3  19125  resgrpisgrp  19128  eqgval  19158  eqger  19159  cycsubgcl  19187  isgim  19243  gim0to0  19250  gaorb  19288  gaorber  19289  gastacos  19291  symg2bas  19372  galactghm  19383  pmtr3ncom  19454  ispgp  19571  efgcpbllema  19733  efgcpbllemb  19734  eqgabl  19813  qusecsub  19814  cygabl  19870  dprdw  19991  rnglz  20123  rngpropd  20132  ringpropd  20246  ringrghm  20271  isirred2  20379  rngcsect  20594  rngcinv  20595  ringcsect  20628  ringcinv  20629  drngid2  20710  issdrg2  20753  islss  20889  islmim  21018  lmhmpropd  21029  zndvds  21508  znleval  21513  znleval2  21514  obselocv  21686  mpfrcl  22041  matinvgcell  22371  mat1dimscm  22411  scmatscm  22449  scmatf1  22467  mdetunilem7  22554  cpmatacl  22652  cpmatmcl  22655  mat2pmatf1  22665  mat2pmatghm  22666  mat2pmatmul  22667  mat2pmatlin  22671  mat2pmatscmxcl  22676  m2pmfzgsumcl  22684  decpmataa0  22704  monmatcollpw  22715  pmatcollpwscmatlem1  22725  pmatcollpwscmatlem2  22726  pm2mpghm  22752  pm2mpmhmlem2  22755  monmat2matmon  22760  chfacfisf  22790  chfacfisfcpmat  22791  chfacfpmmulgsum2  22801  isbasis3g  22885  leordtvallem2  23147  lmfval  23168  lmbr  23194  lmbr2  23195  lmmo  23316  dfconn2  23355  ptbasin  23513  ptbasfi  23517  txcnpi  23544  ptcnp  23558  hausdiag  23581  qtophmeo  23753  fbunfip  23805  elflim2  23900  hausflimi  23916  isfcls  23945  isfcls2  23949  istmd  24010  istgp  24013  istrg  24100  istdrg  24102  istdrg2  24114  istlm  24121  imasdsf1olem  24310  xmeterval  24369  xmeter  24370  prdsxmslem2  24466  blval2  24499  isngp  24533  isngp2  24534  isngp3  24535  isnlm  24612  cnbl0  24710  cnblcld  24711  elii1  24880  isphtpc  24942  phtpcer  24943  isclmp  25046  iscph  25120  lmmbr  25208  lmmbr2  25209  lmmbrf  25212  iscfil2  25216  iscau3  25228  iscau4  25229  iscauf  25230  caucfil  25233  isbn  25288  ishl2  25320  ovolfcl  25417  ioombl1lem4  25512  mbfmax  25600  iblpos  25744  limcrcl  25825  ig1pval3  26133  ulmdvlem3  26361  ellogdm  26598  relogbcl  26733  fsumvma2  27175  chpchtsum  27180  chpub  27181  dchrelbas3  27199  gausslemma2dlem1a  27326  noetalem1  27703  eqscut  27767  eqscut2  27768  lnhl  28540  colopp  28694  dfcgra2  28755  axeuclidlem  28887  axeuclid  28888  edgupgr  29059  umgr2edg1  29136  subusgr  29214  nbgrel  29265  nb3grpr2  29308  nb3gr2nb  29309  isuvtx  29320  nbupgruvtxres  29332  iscplgredg  29342  cplgr3v  29360  rusgrpropedg  29510  rgrusgrprc  29515  rusgrprc  29516  upgriswlk  29567  wlkonprop  29584  wksonproplem  29630  wksonproplemOLD  29631  usgr2pth0  29693  isclwlke  29705  crctcshtrl  29751  iswwlksnx  29768  wwlknbp  29770  2trld  29866  rusgrnumwwlkl1  29896  rusgrnumwwlkb0  29899  rusgrnumwwlk  29903  clwlkclwwlkflem  29931  erclwwlkref  29947  clwwlkwwlksb  29981  erclwwlknref  29996  clwwlknon2x  30030  0wlk  30043  3spthd  30103  umgr3v3e3cycl  30111  frgr3v  30202  1to3vfriswmgr  30207  frgr2wwlkeu  30254  numclwwlk1lem2fo  30285  dlwwlknondlwlknonf1o  30292  nvex  30538  isnv  30539  dfadj2  31812  cnvadj  31819  adjeq  31862  eleigvec  31884  eleigvec2  31885  chirredi  32321  or3di  32386  tpssg  32464  eliccelico  32700  omndmul2  33026  pmtrprfv2  33045  fzto1st  33060  psgnfzto1st  33062  isorng  33267  qusker  33310  qusxpid  33324  lsmsnorb  33352  prmidl0  33411  mxidlirred  33433  ply1degltel  33550  ply1degleel  33551  eulerpartlemv  34342  eulerpartlemd  34344  eulerpartlemn  34359  prob01  34391  probun  34397  bnj170  34675  bnj248  34677  bnj252  34680  bnj253  34681  bnj945  34750  bnj1098  34760  bnj1224  34778  bnj150  34853  bnj153  34857  bnj545  34872  bnj557  34878  bnj571  34883  bnj594  34889  bnj864  34899  bnj865  34900  bnj849  34902  bnj964  34920  bnj986  34932  bnj996  34933  bnj1033  34946  bnj1110  34959  bnj1128  34967  bnj1174  34980  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  35683  br6  35720  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  36551  relowlpssretop  37328  wl-df3-3mintru2  37450  lindsenlbs  37585  matunitlindflem2  37587  fdc  37715  isbnd3b  37755  ablo4pnp  37850  crngm4  37973  isidlc  37985  pridl  38007  ispridl2  38008  ispridlc  38040  ts3an1  38120  ts3an2  38121  ts3an3  38122  brres2  38232  disjressuc2  38352  xrninxp  38356  dfeqvrels2  38552  dfeqvrel2  38554  dfeqvrel3  38555  dfeldisj3  38683  islshpsm  38944  islshpat  38981  cmtfvalN  39174  cmtvalN  39175  ishlat1  39316  ishlat2  39317  3dim0  39422  2dim  39435  islvol5  39544  lhpexle3  39977  cdleme0ex2N  40189  cdleme0nex  40255  cdlemg2cex  40556  cdlemg33b0  40666  cdlemg33b  40672  cdlemg33c  40673  cdlemg33e  40675  dib1dim  41130  diblsmopel  41136  dihopelvalcpre  41213  lcfls1c  41501  aks6d1c1p1  42066  aks6d1c1p1rcl  42067  sn-sup2  42461  sn-isghm  42643  3anrabdioph  42752  fgraphxp  43175  omge2  43269  faosnf0.11b  43398  dfsucon  43494  pren2  43524  dfrtrcl5  43600  brfvrcld2  43663  df3an2  43740  dfvd3  44564  3impexpVD  44828  modelaxreplem1  44951  rfcnnnub  45008  stoweidlem35  46012  smflimlem4  46751  ndmaovass  47183  nltle2tri  47290  elfz2z  47292  prproropf1olem0  47464  reuprpr  47485  gboge9  47726  sbgoldbalt  47743  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  bgoldbtbndlem4  47770  bgoldbtbnd  47771  dfvopnbgr2  47814  isuspgrim  47857  isubgr3stgrlem7  47932  grlimprop2  47946  uhgrimgrlim  47947  rngcsectALTV  48198  rngcinvALTV  48199  ringcsectALTV  48232  ringcinvALTV  48233  islindeps  48377  islindeps2  48407  isldepslvec2  48409  elbigo2  48480  line2ylem  48679  io1ii  48843  catprsc  48936  0funcglem  48996  0funclem  48999  isthincd2  49271  thincsect  49301  2arwcatlem1  49420