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  2379  mopick2  2662  r19.26-3  3123  r3al  3200  r3ex  3201  rexlimdvvva  3220  3reeanv  3235  ceqsex3v  3502  ceqsex4v  3503  ceqsex8v  3505  rspc4v  3595  sbc3an  3802  elin3  4151  rexdifpr  4619  raltpg  4658  tpss  4796  opthprneg  4824  dfopif  4829  disjxun  5100  otth2  5451  otthg  5453  oteqex  5469  poirr  5567  po3nr  5570  wefrc  5641  otelxp  5691  rabxp  5695  f1orn  6823  2f1fvneq  7252  fpropnf1  7259  dff1o6  7271  oprabidw  7439  oprabid  7440  oprabv  7468  ndmovass  7597  elovmpo  7654  elovmporab  7655  elovmporab1w  7656  elovmporab1  7657  elovmpt3rab1  7669  dfwe2  7771  opiota  8053  dfxp3  8055  bropopvvv  8084  poxp2  8138  xpord2pred  8140  xpord3pred  8147  sexp3  8148  oaord  8533  oeeu  8590  nnaord  8606  naddasslem1  8682  swoso  8730  fiint  9296  funsnfsupp  9362  ttrclselem2  9705  alephval3  10160  ingru  10871  axgroth3  10887  ltrelxr  11341  ltxrlt  11351  wloglei  11817  sup2  12242  rexuz2  12995  ltxr  13213  elixx3g  13458  ixxun  13461  dfrp2  13494  elioo4g  13506  elioopnf  13543  elioomnf  13544  elicopnf  13545  elxrge0  13557  divelunit  13594  elfz2  13615  elfzuzb  13619  uzsplit  13698  fznn0  13721  elfzmlbp  13741  preduz  13752  elfzo2  13764  fzolb2  13769  fzouzsplit  13797  ssfzo12bi  13864  fzind2  13891  hashgt23el  14536  ccatsymb  14695  swrdsbslen  14781  swrdspsleq  14782  swrdccatin2  14845  pfxccatin12lem2  14847  pfxccatin12lem3  14848  pfxccatin12  14849  pfxccat3a  14854  repsdf2  14896  repswsymball  14897  repswsymballbi  14898  repswswrd  14902  s3eq3seq  15057  wrdl3s3  15082  s3sndisj  15087  s3iunsndisj  15088  abs2dif  15467  sinltx  16324  divalglem8  16537  divalglem10  16539  divalgb  16541  bitsval2  16562  divgcdz  16648  rplpwr  16695  cncongr1  16804  pythagtriplem2  16956  pythagtrip  16973  prmgaplem4  17193  isstruct  17291  setsstruct2  17313  imasvscafn  17670  xpscf  17698  mreexmrid  17778  iscatd2  17816  issect  17889  issect2  17890  oppcsect  17914  isfunc  18000  funcpropd  18038  fucsect  18111  fucinv  18112  initoeu2  18152  setcsect  18225  setcinv  18226  issgrpd  18880  ismhm0  18946  issubm2  18960  issubg3  19316  resgrpisgrp  19319  eqgval  19350  eqger  19351  qusxpid  19356  cycsubgcl  19382  isgim  19437  gim0to0  19444  gaorb  19482  gaorber  19483  gastacos  19485  symg2bas  19568  galactghm  19579  pmtr3ncom  19650  ispgp  19767  efgcpbllema  19929  efgcpbllemb  19930  eqgabl  20009  qusecsub  20010  cygabl  20066  dprdw  20187  omndmul2  20308  rnglz  20348  rngpropd  20357  ringpropd  20480  ringrghm  20505  isirred2  20612  rngcsect  20849  rngcinv  20850  ringcsect  20883  ringcinv  20884  isdrng5  20969  drngid2  20971  issdrg2  21013  isorng  21079  islss  21170  islmim  21298  lmhmpropd  21309  prmidl0  21595  zndvds  21816  znleval  21821  znleval2  21822  obselocv  21995  lindsenlbs  22118  mpfrcl  22355  matinvgcell  22711  mat1dimscm  22751  scmatscm  22789  scmatf1  22807  mdetunilem7  22894  matunitlindflem2  22956  cpmatacl  22995  cpmatmcl  22998  mat2pmatf1  23008  mat2pmatghm  23009  mat2pmatmul  23010  mat2pmatlin  23014  mat2pmatscmxcl  23019  m2pmfzgsumcl  23027  decpmataa0  23047  monmatcollpw  23058  pmatcollpwscmatlem1  23068  pmatcollpwscmatlem2  23069  pm2mpghm  23095  pm2mpmhmlem2  23098  monmat2matmon  23103  chfacfisf  23133  chfacfisfcpmat  23134  chfacfpmmulgsum2  23144  isbasis3g  23228  leordtvallem2  23490  lmfval  23511  lmbr  23537  lmbr2  23538  lmmo  23659  dfconn2  23698  ptbasin  23857  ptbasfi  23861  txcnpi  23888  ptcnp  23902  hausdiag  23925  qtophmeo  24097  fbunfip  24149  elflim2  24244  hausflimi  24260  isfcls  24289  isfcls2  24293  istmd  24354  istgp  24357  istrg  24444  istdrg  24446  istdrg2  24458  istlm  24465  imasdsf1olem  24653  xmeterval  24712  xmeter  24713  prdsxmslem2  24809  blval2  24842  isngp  24876  isngp2  24877  isngp3  24878  isnlm  24955  cnbl0  25053  cnblcld  25054  elii1  25217  isphtpc  25276  phtpcer  25277  isclmp  25379  iscph  25452  lmmbr  25540  lmmbr2  25541  lmmbrf  25544  iscfil2  25548  iscau3  25560  iscau4  25561  iscauf  25562  caucfil  25565  isbn  25620  ishl2  25652  ovolfcl  25748  ioombl1lem4  25843  mbfmax  25931  iblpos  26074  limcrcl  26155  ig1pval3  26457  ulmdvlem3  26692  ellogdm  26930  relogbcl  27064  fsumvma2  27504  chpchtsum  27509  chpub  27510  dchrelbas3  27528  gausslemma2dlem1a  27655  noetalem1  28031  sltssnb  28088  eqcuts  28104  eqcuts2  28105  lnhl  29014  colopp  29180  dfcgra2  29271  axeuclidlem  29473  axeuclid  29474  edgupgr  29645  umgr2edg1  29725  subusgr  29803  nbgrel  29854  nb3grpr2  29897  nb3gr2nb  29898  isuvtx  29909  nbupgruvtxres  29921  iscplgredg  29931  cplgr3v  29949  rusgrpropedg  30098  rgrusgrprc  30103  rusgrprc  30104  upgriswlk  30154  wlkonprop  30170  subgrwlk  30202  wksonproplem  30220  usgr2pth0  30284  isclwlke  30297  crctcshtrl  30345  iswwlksnx  30362  wwlknbp  30364  2trld  30460  rusgrnumwwlkl1  30493  rusgrnumwwlkb0  30496  rusgrnumwwlk  30500  clwlkclwwlkflem  30528  erclwwlkref  30544  clwwlkwwlksb  30578  erclwwlknref  30593  clwwlknon2x  30627  0wlk  30640  loop1cycl  30677  3spthd  30710  umgr3v3e3cycl  30718  frgr3v  30809  1to3vfriswmgr  30814  frgr2wwlkeu  30861  numclwwlk1lem2fo  30892  dlwwlknondlwlknonf1o  30899  nvex  31146  isnv  31147  dfadj2  32420  cnvadj  32427  adjeq  32470  eleigvec  32492  eleigvec2  32493  chirredi  32929  or3di  32990  tpssg  33066  eliccelico  33302  pmtrprfv2  33582  fzto1st  33597  psgnfzto1st  33599  qusker  33843  lsmsnorb  33879  mxidlirred  33930  ply1degltel  34059  ply1degleel  34060  eulerpartlemv  34930  eulerpartlemd  34932  eulerpartlemn  34947  prob01  34979  probun  34985  bnj170  35263  bnj248  35265  bnj252  35268  bnj253  35269  bnj945  35338  bnj1098  35348  bnj1224  35365  bnj150  35440  bnj153  35444  bnj545  35459  bnj557  35465  bnj571  35470  bnj594  35476  bnj864  35486  bnj865  35487  bnj849  35489  bnj964  35507  bnj986  35519  bnj996  35520  bnj1033  35533  bnj1110  35546  bnj1128  35554  bnj1174  35567  cusgr3cyclex  35832  2cycl2d  35833  pconnconn  35917  resconn  35932  iscvm  35945  cvmlift2lem12  36000  cvmlift3lem5  36009  satfdm  36055  elmpst  36222  mpstrcl  36227  lediv2aALT  36363  3jcadALT  36373  dfso3  36406  br6  36443  elfuns  36599  brimg  36621  lemsuccf  36625  cgrxfr  36742  segcon2  36792  seglecgr12im  36797  seglecgr12  36798  segletr  36801  btwnoutside  36812  broutsideof3  36813  outsideoftr  36816  outsidele  36819  bj-imn3ani  37379  relowlpssretop  38207  wl-df3-3mintru2  38329  fdc  38599  isbnd3b  38639  ablo4pnp  38734  crngm4  38857  isidlc  38869  pridl  38891  ispridl2  38892  ispridlc  38924  ts3an1  39002  ts3an2  39003  ts3an3  39004  brres2  39125  disjressuc2  39263  xrninxp  39267  dfsuccl4  39326  dfeqvrels2  39524  dfeqvrel2  39526  dfeqvrel3  39527  dfeldisj3  39663  islshpsm  39957  islshpat  39994  cmtfvalN  40187  cmtvalN  40188  ishlat1  40329  ishlat2  40330  3dim0  40434  2dim  40447  islvol5  40556  lhpexle3  40989  cdleme0ex2N  41201  cdleme0nex  41267  cdlemg2cex  41568  cdlemg33b0  41678  cdlemg33b  41684  cdlemg33c  41685  cdlemg33e  41687  dib1dim  42142  diblsmopel  42148  dihopelvalcpre  42225  lcfls1c  42513  aks6d1c1p1  43077  aks6d1c1p1rcl  43078  sn-sup2  43483  sn-isghm  43623  3anrabdioph  43731  fgraphxp  44149  omge2  44243  faosnf0.11b  44371  dfsucon  44467  pren2  44497  dfrtrcl5  44573  brfvrcld2  44636  df3an2  44713  dfvd3  45518  3impexpVD  45782  modelaxreplem1  45905  rfcnnnub  45974  stoweidlem35  46967  smflimlem4  47706  ndmaovass  48198  nltle2tri  48305  elfz2z  48307  prproropf1olem0  48506  reuprpr  48527  gboge9  48784  sbgoldbalt  48801  nnsum4primesodd  48816  nnsum4primesoddALTV  48817  bgoldbtbndlem4  48828  bgoldbtbnd  48829  dfvopnbgr2  48873  isuspgrim  48916  isubgr3stgrlem7  48992  grlimprop2  49006  uhgrimgrlim  49007  pgn4cyclex  49146  rngcsectALTV  49294  rngcinvALTV  49295  ringcsectALTV  49328  ringcinvALTV  49329  islindeps  49487  islindeps2  49517  isldepslvec2  49519  elbigo2  49586  line2ylem  49785  io1ii  49951  catprsc  50043  0funcglem  50113  0funclem  50116  catcsect  50428  isthincd2  50467  thincsect  50497  2arwcatlem1  50625