Definition df-3an 1033

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 679. (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 1031	. 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒)
5	1, 2	wa 383	. . 3 wff (𝜑 ∧ 𝜓)
6	5, 3	wa 383	. 2 wff ((𝜑 ∧ 𝜓) ∧ 𝜒)
7	4, 6	wb 195	1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))

This definition is referenced by:  3anass  1035  3anrot  1036  3ancoma  1038  3anan32  1043  3anor  1047  3ioran  1049  3simpa  1051  3pm3.2i  1232  pm3.2an3  1233  pm3.2an3OLD  1234  3jca  1235  3anbi123i  1244  3imp  1249  3an4anass  1283  3anbi123d  1391  3anim123d  1398  an6  1400  an3andi  1437  an33rean  1438  cadan  1539  19.26-3an  1788  nf3and  1815  nf3an  1819  4exdistr  1911  eeeanv  2171  nf3andOLD  2221  nf3anOLD  2227  sb3an  2388  mopick2  2528  r3al  2924  r19.26-3  3048  3reeanv  3087  ceqsex3v  3219  ceqsex4v  3220  ceqsex8v  3222  sbc3an  3461  elin3  3766  raltpg  4183  tpss  4308  dfopif  4337  disjxun  4581  otth2  4878  otthg  4880  oteqex  4889  poirr  4970  po3nr  4973  wefrc  5032  rabxp  5078  brinxp2  5103  brinxp  5104  f1orn  6060  dff1o6  6431  oprabid  6576  oprabv  6601  ndmovass  6720  elovmpt2  6777  elovmpt2rab  6778  elovmpt2rab1  6779  elovmpt3rab1  6791  dfwe2  6873  opiota  7118  dfxp3  7119  bropopvvv  7142  oaord  7514  oeeu  7570  nnaord  7586  swoso  7662  fiint  8122  funsnfsupp  8182  alephval3  8816  fpwwe2lem8  9338  fpwwe2lem9  9339  fpwwe2lem12  9342  ingru  9516  axgroth3  9532  ltrelxr  9978  ltxrlt  9987  wloglei  10439  sup2  10858  rexuz2  11615  ltxr  11825  elixx3g  12059  ixxun  12062  elioo4g  12105  elioopnf  12138  elioomnf  12139  elicopnf  12140  elxrge0  12152  divelunit  12185  elfz2  12204  elfzuzb  12207  uzsplit  12281  fznn0  12301  elfzmlbp  12319  preduz  12330  elfzo2  12342  fzolb2  12346  fzouzsplit  12372  ssfzo12bi  12429  fzind2  12448  ccatsymb  13219  swrdsbslen  13300  swrdspsleq  13301  swrdccatin2  13338  swrdccatin12lem2  13340  swrdccatin12lem3  13341  swrdccatin12  13342  repsdf2  13376  repswsymball  13377  repswsymballbi  13378  repswswrd  13382  wrdl3s3  13553  s3sndisj  13554  s3iunsndisj  13555  abs2dif  13920  sinltx  14758  divalglem8  14961  divalglem10  14963  divalgb  14965  bitsval2  14985  divgcdz  15071  rplpwr  15114  cncongr1  15219  pythagtriplem2  15360  pythagtrip  15377  prmgaplem4  15596  pwsle  15975  imasvscafn  16020  mreexmrid  16126  iscatd2  16165  issect  16236  issect2  16237  oppcsect  16261  isfunc  16347  funcpropd  16383  fucsect  16455  fucinv  16456  initoeu2  16489  setcsect  16562  setcinv  16563  issubm2  17171  issubg3  17435  resgrpisgrp  17438  cycsubgcl  17443  eqgval  17466  eqger  17467  isgim  17527  gaorb  17563  gaorber  17564  gastacos  17566  symg2bas  17641  galactghm  17646  gsmsymgreqlem2  17674  pmtr3ncom  17718  ispgp  17830  efgcpbllema  17990  efgcpbllemb  17991  eqgabl  18063  dprdw  18232  ringpropd  18405  ringrghm  18428  isirred2  18524  rim0to0  18565  drngid2  18586  islss  18756  islmim  18883  lmhmpropd  18894  isassa  19136  mpfrcl  19339  zndvds  19717  znleval  19722  znleval2  19723  obselocv  19891  matinvgcell  20060  mat1dimscm  20100  scmatscm  20138  scmatf1  20156  mdetunilem7  20243  cpmatacl  20340  cpmatmcl  20343  mat2pmatf1  20353  mat2pmatghm  20354  mat2pmatmul  20355  mat2pmatlin  20359  mat2pmatscmxcl  20364  m2pmfzgsumcl  20372  decpmataa0  20392  monmatcollpw  20403  pmatcollpwscmatlem1  20413  pmatcollpwscmatlem2  20414  pm2mpghm  20440  pm2mpmhmlem2  20443  monmat2matmon  20448  chfacfisf  20478  chfacfisfcpmat  20479  chfacfpmmulgsum2  20489  isbasis3g  20564  leordtvallem2  20825  lmfval  20846  lmbr  20872  lmbr2  20873  lmmo  20994  dfcon2  21032  ptbasin  21190  ptbasfi  21194  txcnpi  21221  ptcnp  21235  hausdiag  21258  qtophmeo  21430  fbunfip  21483  elflim2  21578  hausflimi  21594  isfcls  21623  isfcls2  21627  istmd  21688  istgp  21691  istrg  21777  istdrg  21779  istdrg2  21791  istlm  21798  imasdsf1olem  21988  xmeterval  22047  xmeter  22048  prdsxmslem2  22144  blval2  22177  isngp  22210  isngp2  22211  isngp3  22212  isnlm  22289  cnbl0  22387  cnblcld  22388  elii1  22542  isphtpc  22601  phtpcer  22602  phtpcerOLD  22603  isclmp  22705  iscph  22778  lmmbr  22864  lmmbr2  22865  lmmbrf  22868  iscfil2  22872  iscau3  22884  iscau4  22885  iscauf  22886  caucfil  22889  isbn  22943  ishl2  22974  ovolfcl  23042  ioombl1lem4  23136  mbfmax  23222  iblpos  23365  limcrcl  23444  ig1pval3  23738  ulmdvlem3  23960  ellogdm  24185  relogbcl  24311  fsumvma2  24739  chpchtsum  24744  chpub  24745  dchrelbas3  24763  gausslemma2dlem1a  24890  lnhl  25310  colopp  25461  dfcgra2  25521  axeuclidlem  25642  axeuclid  25643  edgupgr  25808  nb3grapr2  25983  nb3gra2nb  25984  0wlk  26075  0trl  26076  constr2wlk  26128  3v3e3cycl1  26172  wwlknred  26251  wwlknndef  26265  isclwlk  26284  clwwlkprop  26298  clwwlknndef  26301  clwwlknwwlkncl  26328  wwlkext2clwwlk  26331  wwlksubclwwlk  26332  clwwnisshclwwn  26337  erclwwlkref  26341  erclwwlknref  26353  clwlkfoclwwlk  26372  el2wlkonotot0  26399  el2wlkonotot  26400  el2wlkonotot1  26401  2wlkonotv  26404  usg2spthonot0  26416  cusgraisrusgra  26465  rusgranumwlkl1  26474  rusgranumwlkb0  26480  rusgra0edg  26482  rusgranumwlk  26484  frgra3v  26529  1to3vfriswmgra  26534  frgraregorufrg  26599  extwwlkfablem2  26605  numclwwlkffin  26609  numclwwlkovfel2  26610  numclwwlkovf2  26611  numclwwlkovf2ex  26613  numclwwlkovgelim  26616  numclwlk1lem2fo  26622  numclwwlk2lem1  26629  numclwwlk7  26641  nvex  26850  isnv  26851  dfadj2  28128  cnvadj  28135  adjeq  28178  eleigvec  28200  eleigvec2  28201  chirredi  28637  or3di  28691  dfrp2  28922  eliccelico  28929  omndmul2  29043  isorng  29130  pmtrprfv2  29179  fzto1st  29184  psgnfzto1st  29186  eulerpartlemv  29753  eulerpartlemd  29755  eulerpartlemn  29770  prob01  29802  probun  29808  bnj170  30017  bnj248  30019  bnj252  30022  bnj253  30023  bnj945  30098  bnj1098  30108  bnj1224  30126  bnj150  30200  bnj153  30204  bnj545  30219  bnj557  30225  bnj571  30230  bnj594  30236  bnj864  30246  bnj865  30247  bnj849  30249  bnj964  30267  bnj986  30278  bnj996  30279  bnj1033  30291  bnj1110  30304  bnj1128  30312  bnj1174  30325  pconcon  30467  rescon  30482  iscvm  30495  cvmlift2lem12  30550  cvmlift3lem5  30559  elmpst  30687  mpstrcl  30692  lediv2aALT  30825  dfso3  30856  br6  30900  nofulllem2  31102  nofulllem5  31105  elfuns  31192  brimg  31214  brsuccf  31218  cgrxfr  31332  segcon2  31382  seglecgr12im  31387  seglecgr12  31388  segletr  31391  btwnoutside  31402  broutsideof3  31403  outsideoftr  31406  outsidele  31409  bj-imn3ani  31745  relowlpssretop  32388  lindsenlbs  32574  matunitlindflem2  32576  fdc  32711  isbnd3b  32754  ablo4pnp  32849  crngm4  32972  isidlc  32984  pridl  33006  ispridl2  33007  ispridlc  33039  ts3an1  33127  ts3an2  33128  ts3an3  33129  islshpsm  33285  islshpat  33322  cmtfvalN  33515  cmtvalN  33516  ishlat1  33657  ishlat2  33658  3dim0  33761  2dim  33774  islvol5  33883  lhpexle3  34316  cdleme0ex2N  34529  cdleme0nex  34595  cdlemg2cex  34897  cdlemg33b0  35007  cdlemg33b  35013  cdlemg33c  35014  cdlemg33e  35016  dib1dim  35472  diblsmopel  35478  dihopelvalcpre  35555  lcfls1c  35843  3anrabdioph  36364  issdrg2  36787  fgraphxp  36808  dfrtrcl5  36955  brfvrcld2  37003  df3an2  37080  dfvd3  37828  3impexpVD  38113  rfcnnnub  38218  stoweidlem35  38928  smflimlem4  39660  ndmaovass  39935  nltle2tri  39942  gboage9  40186  sgoldbalt  40203  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  bgoldbtbndlem4  40224  bgoldbtbnd  40225  pfxccatin12lem2  40287  pfxccatin12  40288  pfxccat3a  40292  rexdifpr  40315  fpropnf1  40337  elfz2z  40352  umgr2edg1  40438  subusgr  40513  nb3grpr2  40611  nb3gr2nb  40612  isuvtxa  40621  nbupgruvtxres  40634  iscplgredg  40639  cplgr3v  40657  rusgrpropedg  40784  rgrusgrprc  40789  rusgrprc  40790  wlkOnprop  40866  lfgriswlk  40897  1wlksonproplem  40912  usgr2pth0  40971  isclWlke  40984  crctcshtrl  41026  iswwlksnx  41042  wwlknbp  41044  2trld  41145  rusgrnumwwlkl1  41172  rusgrnumwwlkb0  41174  rusgrnumwwlk  41178  erclwwlksref  41241  erclwwlksnref  41253  clwlksf1clwwlklem0  41271  01wlk  41284  3spthd  41343  umgr3v3e3cycl  41351  frgr3v  41445  1to3vfriswmgr  41450  frgr2wwlkeu  41492  av-extwwlkfablem2  41510  av-numclwwlkovfel2  41514  av-numclwwlkovf2  41515  av-numclwlk1lem2fo  41525  ismhm0  41595  rnglz  41674  rngcsect  41772  rngcinv  41773  rngcsectALTV  41784  rngcinvALTV  41785  ringcsect  41823  ringcinv  41824  ringcsectALTV  41847  ringcinvALTV  41848  islindeps  42036  islindeps2  42066  isldepslvec2  42068  elbigo2  42144