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  2082  eeeanv  2348  mopick2  2630  r19.26-3  3092  r3al  3175  r3ex  3176  rexlimdvvva  3195  3reeanv  3210  ceqsex3v  3503  ceqsex4v  3504  ceqsex8v  3506  rspc4v  3608  sbc3an  3818  elin3  4169  rexdifpr  4623  raltpg  4662  tpss  4801  opthprneg  4829  dfopif  4834  disjxun  5105  otth2  5443  otthg  5445  oteqex  5460  poirr  5558  po3nr  5561  wefrc  5632  otelxp  5682  rabxp  5686  f1orn  6810  2f1fvneq  7235  fpropnf1  7242  dff1o6  7250  oprabidw  7418  oprabid  7419  oprabv  7449  ndmovass  7577  elovmpo  7634  elovmporab  7635  elovmporab1w  7636  elovmporab1  7637  elovmpt3rab1  7649  dfwe2  7750  opiota  8038  dfxp3  8040  bropopvvv  8069  poxp2  8122  xpord2pred  8124  xpord3pred  8131  sexp3  8132  oaord  8511  oeeu  8567  nnaord  8583  naddasslem1  8658  swoso  8705  fiint  9277  fiintOLD  9278  funsnfsupp  9343  ttrclselem2  9679  alephval3  10063  ingru  10768  axgroth3  10784  ltrelxr  11235  ltxrlt  11244  wloglei  11710  sup2  12139  rexuz2  12858  ltxr  13075  elixx3g  13319  ixxun  13322  dfrp2  13355  elioo4g  13367  elioopnf  13404  elioomnf  13405  elicopnf  13406  elxrge0  13418  divelunit  13455  elfz2  13475  elfzuzb  13479  uzsplit  13557  fznn0  13580  elfzmlbp  13600  preduz  13611  elfzo2  13623  fzolb2  13627  fzouzsplit  13655  ssfzo12bi  13722  fzind2  13746  hashgt23el  14389  ccatsymb  14547  swrdsbslen  14629  swrdspsleq  14630  swrdccatin2  14694  pfxccatin12lem2  14696  pfxccatin12lem3  14697  pfxccatin12  14698  pfxccat3a  14703  repsdf2  14743  repswsymball  14744  repswsymballbi  14745  repswswrd  14749  s3eq3seq  14905  wrdl3s3  14928  s3sndisj  14933  s3iunsndisj  14934  abs2dif  15299  sinltx  16157  divalglem8  16370  divalglem10  16372  divalgb  16374  bitsval2  16395  divgcdz  16481  rplpwr  16528  cncongr1  16637  pythagtriplem2  16788  pythagtrip  16805  prmgaplem4  17025  isstruct  17122  setsstruct2  17144  imasvscafn  17500  xpscf  17528  mreexmrid  17604  iscatd2  17642  issect  17715  issect2  17716  oppcsect  17740  isfunc  17826  funcpropd  17864  fucsect  17937  fucinv  17938  initoeu2  17978  setcsect  18051  setcinv  18052  issgrpd  18657  ismhm0  18717  issubm2  18731  issubg3  19076  resgrpisgrp  19079  eqgval  19109  eqger  19110  cycsubgcl  19138  isgim  19194  gim0to0  19201  gaorb  19239  gaorber  19240  gastacos  19242  symg2bas  19323  galactghm  19334  pmtr3ncom  19405  ispgp  19522  efgcpbllema  19684  efgcpbllemb  19685  eqgabl  19764  qusecsub  19765  cygabl  19821  dprdw  19942  rnglz  20074  rngpropd  20083  ringpropd  20197  ringrghm  20222  isirred2  20330  rngcsect  20545  rngcinv  20546  ringcsect  20579  ringcinv  20580  drngid2  20661  issdrg2  20704  islss  20840  islmim  20969  lmhmpropd  20980  zndvds  21459  znleval  21464  znleval2  21465  obselocv  21637  mpfrcl  21992  matinvgcell  22322  mat1dimscm  22362  scmatscm  22400  scmatf1  22418  mdetunilem7  22505  cpmatacl  22603  cpmatmcl  22606  mat2pmatf1  22616  mat2pmatghm  22617  mat2pmatmul  22618  mat2pmatlin  22622  mat2pmatscmxcl  22627  m2pmfzgsumcl  22635  decpmataa0  22655  monmatcollpw  22666  pmatcollpwscmatlem1  22676  pmatcollpwscmatlem2  22677  pm2mpghm  22703  pm2mpmhmlem2  22706  monmat2matmon  22711  chfacfisf  22741  chfacfisfcpmat  22742  chfacfpmmulgsum2  22752  isbasis3g  22836  leordtvallem2  23098  lmfval  23119  lmbr  23145  lmbr2  23146  lmmo  23267  dfconn2  23306  ptbasin  23464  ptbasfi  23468  txcnpi  23495  ptcnp  23509  hausdiag  23532  qtophmeo  23704  fbunfip  23756  elflim2  23851  hausflimi  23867  isfcls  23896  isfcls2  23900  istmd  23961  istgp  23964  istrg  24051  istdrg  24053  istdrg2  24065  istlm  24072  imasdsf1olem  24261  xmeterval  24320  xmeter  24321  prdsxmslem2  24417  blval2  24450  isngp  24484  isngp2  24485  isngp3  24486  isnlm  24563  cnbl0  24661  cnblcld  24662  elii1  24831  isphtpc  24893  phtpcer  24894  isclmp  24997  iscph  25070  lmmbr  25158  lmmbr2  25159  lmmbrf  25162  iscfil2  25166  iscau3  25178  iscau4  25179  iscauf  25180  caucfil  25183  isbn  25238  ishl2  25270  ovolfcl  25367  ioombl1lem4  25462  mbfmax  25550  iblpos  25694  limcrcl  25775  ig1pval3  26083  ulmdvlem3  26311  ellogdm  26548  relogbcl  26683  fsumvma2  27125  chpchtsum  27130  chpub  27131  dchrelbas3  27149  gausslemma2dlem1a  27276  noetalem1  27653  eqscut  27717  eqscut2  27718  lnhl  28542  colopp  28696  dfcgra2  28757  axeuclidlem  28889  axeuclid  28890  edgupgr  29061  umgr2edg1  29138  subusgr  29216  nbgrel  29267  nb3grpr2  29310  nb3gr2nb  29311  isuvtx  29322  nbupgruvtxres  29334  iscplgredg  29344  cplgr3v  29362  rusgrpropedg  29512  rgrusgrprc  29517  rusgrprc  29518  upgriswlk  29569  wlkonprop  29586  wksonproplem  29632  wksonproplemOLD  29633  usgr2pth0  29695  isclwlke  29707  crctcshtrl  29753  iswwlksnx  29770  wwlknbp  29772  2trld  29868  rusgrnumwwlkl1  29898  rusgrnumwwlkb0  29901  rusgrnumwwlk  29905  clwlkclwwlkflem  29933  erclwwlkref  29949  clwwlkwwlksb  29983  erclwwlknref  29998  clwwlknon2x  30032  0wlk  30045  3spthd  30105  umgr3v3e3cycl  30113  frgr3v  30204  1to3vfriswmgr  30209  frgr2wwlkeu  30256  numclwwlk1lem2fo  30287  dlwwlknondlwlknonf1o  30294  nvex  30540  isnv  30541  dfadj2  31814  cnvadj  31821  adjeq  31864  eleigvec  31886  eleigvec2  31887  chirredi  32323  or3di  32388  tpssg  32466  eliccelico  32700  omndmul2  33026  pmtrprfv2  33045  fzto1st  33060  psgnfzto1st  33062  isorng  33277  qusker  33320  qusxpid  33334  lsmsnorb  33362  prmidl0  33421  mxidlirred  33443  ply1degltel  33560  ply1degleel  33561  eulerpartlemv  34355  eulerpartlemd  34357  eulerpartlemn  34372  prob01  34404  probun  34410  bnj170  34688  bnj248  34690  bnj252  34693  bnj253  34694  bnj945  34763  bnj1098  34773  bnj1224  34791  bnj150  34866  bnj153  34870  bnj545  34885  bnj557  34891  bnj571  34896  bnj594  34902  bnj864  34912  bnj865  34913  bnj849  34915  bnj964  34933  bnj986  34945  bnj996  34946  bnj1033  34959  bnj1110  34972  bnj1128  34980  bnj1174  34993  subgrwlk  35119  cusgr3cyclex  35123  loop1cycl  35124  2cycl2d  35126  pconnconn  35218  resconn  35233  iscvm  35246  cvmlift2lem12  35301  cvmlift3lem5  35310  satfdm  35356  elmpst  35523  mpstrcl  35528  lediv2aALT  35664  3jcadALT  35674  dfso3  35707  br6  35744  elfuns  35903  brimg  35925  brsuccf  35929  cgrxfr  36043  segcon2  36093  seglecgr12im  36098  seglecgr12  36099  segletr  36102  btwnoutside  36113  broutsideof3  36114  outsideoftr  36117  outsidele  36120  bj-imn3ani  36575  relowlpssretop  37352  wl-df3-3mintru2  37474  lindsenlbs  37609  matunitlindflem2  37611  fdc  37739  isbnd3b  37779  ablo4pnp  37874  crngm4  37997  isidlc  38009  pridl  38031  ispridl2  38032  ispridlc  38064  ts3an1  38144  ts3an2  38145  ts3an3  38146  brres2  38257  disjressuc2  38374  xrninxp  38378  dfeqvrels2  38579  dfeqvrel2  38581  dfeqvrel3  38582  dfeldisj3  38711  islshpsm  38973  islshpat  39010  cmtfvalN  39203  cmtvalN  39204  ishlat1  39345  ishlat2  39346  3dim0  39451  2dim  39464  islvol5  39573  lhpexle3  40006  cdleme0ex2N  40218  cdleme0nex  40284  cdlemg2cex  40585  cdlemg33b0  40695  cdlemg33b  40701  cdlemg33c  40702  cdlemg33e  40704  dib1dim  41159  diblsmopel  41165  dihopelvalcpre  41242  lcfls1c  41530  aks6d1c1p1  42095  aks6d1c1p1rcl  42096  sn-sup2  42479  sn-isghm  42661  3anrabdioph  42770  fgraphxp  43193  omge2  43287  faosnf0.11b  43416  dfsucon  43512  pren2  43542  dfrtrcl5  43618  brfvrcld2  43681  df3an2  43758  dfvd3  44581  3impexpVD  44845  modelaxreplem1  44968  rfcnnnub  45030  stoweidlem35  46033  smflimlem4  46772  ndmaovass  47207  nltle2tri  47314  elfz2z  47316  prproropf1olem0  47503  reuprpr  47524  gboge9  47765  sbgoldbalt  47782  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  bgoldbtbndlem4  47809  bgoldbtbnd  47810  dfvopnbgr2  47853  isuspgrim  47896  isubgr3stgrlem7  47971  grlimprop2  47985  uhgrimgrlim  47986  pgn4cyclex  48116  rngcsectALTV  48263  rngcinvALTV  48264  ringcsectALTV  48297  ringcinvALTV  48298  islindeps  48442  islindeps2  48472  isldepslvec2  48474  elbigo2  48541  line2ylem  48740  io1ii  48909  catprsc  49002  0funcglem  49072  0funclem  49075  catcsect  49387  isthincd2  49426  thincsect  49456  2arwcatlem1  49584