Definition df-3an 1085

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 471. (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 1083	. 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒)
5	1, 2	wa 398	. . 3 wff (𝜑 ∧ 𝜓)
6	5, 3	wa 398	. 2 wff ((𝜑 ∧ 𝜓) ∧ 𝜒)
7	4, 6	wb 208	1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))

This definition is referenced by:  3anass  1091  3anan32  1093  3ancomb  1095  3anidm  1100  3an4anass  1101  3ioran  1102  3ianor  1103  3impa  1106  3expa  1114  3jca  1124  3anbi123i  1151  3pm3.2i  1335  3anbi123d  1432  3anim123d  1439  an6  1441  an3andi  1478  an33rean  1479  an33reanOLD  1480  cadan  1610  19.26-3an  1873  nf3and  1899  nf3an  1902  4exdistr  1963  sb3an  2087  eeeanv  2371  mopick2  2722  r19.26-3  3172  r3al  3202  3reeanv  3368  ceqsex3v  3545  ceqsex4v  3546  ceqsex8v  3548  sbc3an  3838  elin3  4177  rexdifpr  4598  raltpg  4634  tpss  4768  opthprneg  4795  dfopif  4800  disjxun  5064  otth2  5375  otthg  5377  oteqex  5390  poirr  5485  po3nr  5488  wefrc  5549  rabxp  5600  f1orn  6625  fpropnf1  7025  dff1o6  7032  oprabidw  7187  oprabid  7188  oprabv  7214  ndmovass  7336  elovmpo  7390  elovmporab  7391  elovmporab1w  7392  elovmporab1  7393  elovmpt3rab1  7405  dfwe2  7496  opiota  7757  dfxp3  7759  bropopvvv  7785  oaord  8173  oeeu  8229  nnaord  8245  swoso  8322  fiint  8795  funsnfsupp  8857  alephval3  9536  ingru  10237  axgroth3  10253  ltrelxr  10702  ltxrlt  10711  wloglei  11172  sup2  11597  rexuz2  12300  ltxr  12511  elixx3g  12752  ixxun  12755  elioo4g  12798  elioopnf  12832  elioomnf  12833  elicopnf  12834  elxrge0  12846  divelunit  12881  elfz2  12900  elfzuzb  12903  uzsplit  12980  fznn0  13000  elfzmlbp  13019  preduz  13030  elfzo2  13042  fzolb2  13046  fzouzsplit  13073  ssfzo12bi  13133  fzind2  13156  hashgt23el  13786  ccatsymb  13936  swrdsbslen  14026  swrdspsleq  14027  swrdccatin2  14091  pfxccatin12lem2  14093  pfxccatin12lem3  14094  pfxccatin12  14095  pfxccat3a  14100  repsdf2  14140  repswsymball  14141  repswsymballbi  14142  repswswrd  14146  s3eq3seq  14301  wrdl3s3  14326  s3sndisj  14327  s3iunsndisj  14328  abs2dif  14692  sinltx  15542  divalglem8  15751  divalglem10  15753  divalgb  15755  bitsval2  15774  divgcdz  15860  rplpwr  15907  cncongr1  16011  pythagtriplem2  16154  pythagtrip  16171  prmgaplem4  16390  isstruct  16496  setsstruct2  16521  imasvscafn  16810  xpscf  16838  mreexmrid  16914  iscatd2  16952  issect  17023  issect2  17024  oppcsect  17048  isfunc  17134  funcpropd  17170  fucsect  17242  fucinv  17243  initoeu2  17276  setcsect  17349  setcinv  17350  issubm2  17969  issubg3  18297  resgrpisgrp  18300  eqgval  18329  eqger  18330  cycsubgcl  18349  isgim  18402  gaorb  18437  gaorber  18438  gastacos  18440  symg2bas  18521  galactghm  18532  pmtr3ncom  18603  ispgp  18717  efgcpbllema  18880  efgcpbllemb  18881  eqgabl  18955  cygabl  19010  dprdw  19132  ringpropd  19332  ringrghm  19355  isirred2  19451  gim0to0  19495  rim0to0OLD  19496  drngid2  19518  issdrg2  19577  islss  19706  islmim  19834  lmhmpropd  19845  isassa  20088  mpfrcl  20298  zndvds  20696  znleval  20701  znleval2  20702  obselocv  20872  matinvgcell  21044  mat1dimscm  21084  scmatscm  21122  scmatf1  21140  mdetunilem7  21227  cpmatacl  21324  cpmatmcl  21327  mat2pmatf1  21337  mat2pmatghm  21338  mat2pmatmul  21339  mat2pmatlin  21343  mat2pmatscmxcl  21348  m2pmfzgsumcl  21356  decpmataa0  21376  monmatcollpw  21387  pmatcollpwscmatlem1  21397  pmatcollpwscmatlem2  21398  pm2mpghm  21424  pm2mpmhmlem2  21427  monmat2matmon  21432  chfacfisf  21462  chfacfisfcpmat  21463  chfacfpmmulgsum2  21473  isbasis3g  21557  leordtvallem2  21819  lmfval  21840  lmbr  21866  lmbr2  21867  lmmo  21988  dfconn2  22027  ptbasin  22185  ptbasfi  22189  txcnpi  22216  ptcnp  22230  hausdiag  22253  qtophmeo  22425  fbunfip  22477  elflim2  22572  hausflimi  22588  isfcls  22617  isfcls2  22621  istmd  22682  istgp  22685  istrg  22772  istdrg  22774  istdrg2  22786  istlm  22793  imasdsf1olem  22983  xmeterval  23042  xmeter  23043  prdsxmslem2  23139  blval2  23172  isngp  23205  isngp2  23206  isngp3  23207  isnlm  23284  cnbl0  23382  cnblcld  23383  elii1  23539  isphtpc  23598  phtpcer  23599  isclmp  23701  iscph  23774  lmmbr  23861  lmmbr2  23862  lmmbrf  23865  iscfil2  23869  iscau3  23881  iscau4  23882  iscauf  23883  caucfil  23886  isbn  23941  ishl2  23973  ovolfcl  24067  ioombl1lem4  24162  mbfmax  24250  iblpos  24393  limcrcl  24472  ig1pval3  24768  ulmdvlem3  24990  ellogdm  25222  relogbcl  25351  fsumvma2  25790  chpchtsum  25795  chpub  25796  dchrelbas3  25814  gausslemma2dlem1a  25941  lnhl  26401  colopp  26555  dfcgra2  26616  axeuclidlem  26748  axeuclid  26749  edgupgr  26919  umgr2edg1  26993  subusgr  27071  nbgrel  27122  nb3grpr2  27165  nb3gr2nb  27166  isuvtx  27177  nbupgruvtxres  27189  iscplgredg  27199  cplgr3v  27217  rusgrpropedg  27366  rgrusgrprc  27371  rusgrprc  27372  upgriswlk  27422  wlkonprop  27440  wksonproplem  27486  usgr2pth0  27546  isclwlke  27558  crctcshtrl  27601  iswwlksnx  27618  wwlknbp  27620  2trld  27717  rusgrnumwwlkl1  27747  rusgrnumwwlkb0  27750  rusgrnumwwlk  27754  clwlkclwwlkflem  27782  erclwwlkref  27798  clwwlkwwlksb  27833  erclwwlknref  27848  clwwlknon2x  27882  0wlk  27895  3spthd  27955  umgr3v3e3cycl  27963  frgr3v  28054  1to3vfriswmgr  28059  frgr2wwlkeu  28106  numclwwlk1lem2fo  28137  dlwwlknondlwlknonf1o  28144  nvex  28388  isnv  28389  dfadj2  29662  cnvadj  29669  adjeq  29712  eleigvec  29734  eleigvec2  29735  chirredi  30171  or3di  30225  dfrp2  30491  eliccelico  30500  omndmul2  30713  pmtrprfv2  30732  fzto1st  30745  psgnfzto1st  30747  isorng  30872  qusker  30918  qusxpid  30928  lsmsnorb  30945  eulerpartlemv  31622  eulerpartlemd  31624  eulerpartlemn  31639  prob01  31671  probun  31677  bnj170  31968  bnj248  31970  bnj252  31973  bnj253  31974  bnj945  32045  bnj1098  32055  bnj1224  32073  bnj150  32148  bnj153  32152  bnj545  32167  bnj557  32173  bnj571  32178  bnj594  32184  bnj864  32194  bnj865  32195  bnj849  32197  bnj964  32215  bnj986  32227  bnj996  32228  bnj1033  32241  bnj1110  32254  bnj1128  32262  bnj1174  32275  subgrwlk  32379  cusgr3cyclex  32383  loop1cycl  32384  2cycl2d  32386  pconnconn  32478  resconn  32493  iscvm  32506  cvmlift2lem12  32561  cvmlift3lem5  32570  satfdm  32616  elmpst  32783  mpstrcl  32788  lediv2aALT  32920  dfso3  32950  br6  32993  etasslt  33274  elfuns  33376  brimg  33398  brsuccf  33402  cgrxfr  33516  segcon2  33566  seglecgr12im  33571  seglecgr12  33572  segletr  33575  btwnoutside  33586  broutsideof3  33587  outsideoftr  33590  outsidele  33593  bj-imn3ani  33921  relowlpssretop  34648  lindsenlbs  34902  matunitlindflem2  34904  fdc  35035  isbnd3b  35078  ablo4pnp  35173  crngm4  35296  isidlc  35308  pridl  35330  ispridl2  35331  ispridlc  35363  ts3an1  35443  ts3an2  35444  ts3an3  35445  brres2  35544  xrninxp  35655  dfeqvrels2  35838  dfeqvrel2  35840  dfeqvrel3  35841  dfeldisj3  35967  islshpsm  36131  islshpat  36168  cmtfvalN  36361  cmtvalN  36362  ishlat1  36503  ishlat2  36504  3dim0  36608  2dim  36621  islvol5  36730  lhpexle3  37163  cdleme0ex2N  37375  cdleme0nex  37441  cdlemg2cex  37742  cdlemg33b0  37852  cdlemg33b  37858  cdlemg33c  37859  cdlemg33e  37861  dib1dim  38316  diblsmopel  38322  dihopelvalcpre  38399  lcfls1c  38687  3anrabdioph  39428  fgraphxp  39860  dfsucon  39938  pren2  39961  dfrtrcl5  40038  brfvrcld2  40086  df3an2  40163  dfvd3  40974  3impexpVD  41239  rfcnnnub  41342  stoweidlem35  42369  smflimlem4  43099  ndmaovass  43454  nltle2tri  43562  elfz2z  43564  prproropf1olem0  43713  reuprpr  43734  gboge9  43978  sbgoldbalt  43995  nnsum4primesodd  44010  nnsum4primesoddALTV  44011  bgoldbtbndlem4  44022  bgoldbtbnd  44023  ismhm0  44121  rnglz  44204  rngcsect  44300  rngcinv  44301  rngcsectALTV  44312  rngcinvALTV  44313  ringcsect  44351  ringcinv  44352  ringcsectALTV  44375  ringcinvALTV  44376  islindeps  44557  islindeps2  44587  isldepslvec2  44589  elbigo2  44661  line2ylem  44787