Definition df-3an 1089

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 1087	. 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  1095  3anan32  1097  3ancomb  1099  3anidm  1104  3an4anass  1105  3ioran  1106  3ianor  1107  3impa  1110  3expa  1119  3jca  1129  3anbi123i  1156  3pm3.2i  1341  3jaob  1429  3anbi123d  1439  3anim123d  1446  an6  1448  an3andi  1485  an33rean  1486  cadan  1611  19.26-3an  1874  nf3and  1900  nf3an  1903  4exdistr  1963  sb3an  2087  eeeanv  2355  mopick2  2638  r19.26-3  3099  r3al  3176  r3ex  3177  rexlimdvvva  3196  3reeanv  3211  ceqsex3v  3484  ceqsex4v  3485  ceqsex8v  3487  rspc4v  3585  sbc3an  3794  elin3  4147  rexdifpr  4604  raltpg  4643  tpss  4781  opthprneg  4809  dfopif  4814  disjxun  5084  otth2  5435  otthg  5437  oteqex  5452  poirr  5548  po3nr  5551  wefrc  5622  otelxp  5672  rabxp  5676  f1orn  6788  2f1fvneq  7212  fpropnf1  7219  dff1o6  7227  oprabidw  7395  oprabid  7396  oprabv  7424  ndmovass  7552  elovmpo  7609  elovmporab  7610  elovmporab1w  7611  elovmporab1  7612  elovmpt3rab1  7624  dfwe2  7725  opiota  8009  dfxp3  8011  bropopvvv  8037  poxp2  8090  xpord2pred  8092  xpord3pred  8099  sexp3  8100  oaord  8479  oeeu  8536  nnaord  8552  naddasslem1  8627  swoso  8675  fiint  9234  funsnfsupp  9302  ttrclselem2  9644  alephval3  10029  ingru  10735  axgroth3  10751  ltrelxr  11203  ltxrlt  11213  wloglei  11679  sup2  12109  rexuz2  12846  ltxr  13063  elixx3g  13308  ixxun  13311  dfrp2  13344  elioo4g  13356  elioopnf  13393  elioomnf  13394  elicopnf  13395  elxrge0  13407  divelunit  13444  elfz2  13465  elfzuzb  13469  uzsplit  13547  fznn0  13570  elfzmlbp  13590  preduz  13601  elfzo2  13613  fzolb2  13618  fzouzsplit  13646  ssfzo12bi  13713  fzind2  13740  hashgt23el  14383  ccatsymb  14542  swrdsbslen  14624  swrdspsleq  14625  swrdccatin2  14688  pfxccatin12lem2  14690  pfxccatin12lem3  14691  pfxccatin12  14692  pfxccat3a  14697  repsdf2  14737  repswsymball  14738  repswsymballbi  14739  repswswrd  14743  s3eq3seq  14898  wrdl3s3  14921  s3sndisj  14926  s3iunsndisj  14927  abs2dif  15292  sinltx  16153  divalglem8  16366  divalglem10  16368  divalgb  16370  bitsval2  16391  divgcdz  16477  rplpwr  16524  cncongr1  16633  pythagtriplem2  16785  pythagtrip  16802  prmgaplem4  17022  isstruct  17119  setsstruct2  17141  imasvscafn  17498  xpscf  17526  mreexmrid  17606  iscatd2  17644  issect  17717  issect2  17718  oppcsect  17742  isfunc  17828  funcpropd  17866  fucsect  17939  fucinv  17940  initoeu2  17980  setcsect  18053  setcinv  18054  issgrpd  18695  ismhm0  18755  issubm2  18769  issubg3  19117  resgrpisgrp  19120  eqgval  19149  eqger  19150  cycsubgcl  19178  isgim  19234  gim0to0  19241  gaorb  19279  gaorber  19280  gastacos  19282  symg2bas  19365  galactghm  19376  pmtr3ncom  19447  ispgp  19564  efgcpbllema  19726  efgcpbllemb  19727  eqgabl  19806  qusecsub  19807  cygabl  19863  dprdw  19984  omndmul2  20105  rnglz  20143  rngpropd  20152  ringpropd  20266  ringrghm  20291  isirred2  20398  rngcsect  20610  rngcinv  20611  ringcsect  20644  ringcinv  20645  drngid2  20726  issdrg2  20769  isorng  20835  islss  20926  islmim  21054  lmhmpropd  21065  zndvds  21526  znleval  21531  znleval2  21532  obselocv  21705  mpfrcl  22060  matinvgcell  22397  mat1dimscm  22437  scmatscm  22475  scmatf1  22493  mdetunilem7  22580  cpmatacl  22678  cpmatmcl  22681  mat2pmatf1  22691  mat2pmatghm  22692  mat2pmatmul  22693  mat2pmatlin  22697  mat2pmatscmxcl  22702  m2pmfzgsumcl  22710  decpmataa0  22730  monmatcollpw  22741  pmatcollpwscmatlem1  22751  pmatcollpwscmatlem2  22752  pm2mpghm  22778  pm2mpmhmlem2  22781  monmat2matmon  22786  chfacfisf  22816  chfacfisfcpmat  22817  chfacfpmmulgsum2  22827  isbasis3g  22911  leordtvallem2  23173  lmfval  23194  lmbr  23220  lmbr2  23221  lmmo  23342  dfconn2  23381  ptbasin  23539  ptbasfi  23543  txcnpi  23570  ptcnp  23584  hausdiag  23607  qtophmeo  23779  fbunfip  23831  elflim2  23926  hausflimi  23942  isfcls  23971  isfcls2  23975  istmd  24036  istgp  24039  istrg  24126  istdrg  24128  istdrg2  24140  istlm  24147  imasdsf1olem  24335  xmeterval  24394  xmeter  24395  prdsxmslem2  24491  blval2  24524  isngp  24558  isngp2  24559  isngp3  24560  isnlm  24637  cnbl0  24735  cnblcld  24736  elii1  24899  isphtpc  24958  phtpcer  24959  isclmp  25061  iscph  25134  lmmbr  25222  lmmbr2  25223  lmmbrf  25226  iscfil2  25230  iscau3  25242  iscau4  25243  iscauf  25244  caucfil  25247  isbn  25302  ishl2  25334  ovolfcl  25430  ioombl1lem4  25525  mbfmax  25613  iblpos  25757  limcrcl  25838  ig1pval3  26140  ulmdvlem3  26364  ellogdm  26600  relogbcl  26734  fsumvma2  27174  chpchtsum  27179  chpub  27180  dchrelbas3  27198  gausslemma2dlem1a  27325  noetalem1  27702  sltssnb  27758  eqcuts  27774  eqcuts2  27775  lnhl  28680  colopp  28834  dfcgra2  28895  axeuclidlem  29028  axeuclid  29029  edgupgr  29200  umgr2edg1  29277  subusgr  29355  nbgrel  29406  nb3grpr2  29449  nb3gr2nb  29450  isuvtx  29461  nbupgruvtxres  29473  iscplgredg  29483  cplgr3v  29501  rusgrpropedg  29650  rgrusgrprc  29655  rusgrprc  29656  upgriswlk  29706  wlkonprop  29722  wksonproplem  29768  usgr2pth0  29830  isclwlke  29842  crctcshtrl  29888  iswwlksnx  29905  wwlknbp  29907  2trld  30003  rusgrnumwwlkl1  30036  rusgrnumwwlkb0  30039  rusgrnumwwlk  30043  clwlkclwwlkflem  30071  erclwwlkref  30087  clwwlkwwlksb  30121  erclwwlknref  30136  clwwlknon2x  30170  0wlk  30183  3spthd  30243  umgr3v3e3cycl  30251  frgr3v  30342  1to3vfriswmgr  30347  frgr2wwlkeu  30394  numclwwlk1lem2fo  30425  dlwwlknondlwlknonf1o  30432  nvex  30679  isnv  30680  dfadj2  31953  cnvadj  31960  adjeq  32003  eleigvec  32025  eleigvec2  32026  chirredi  32462  or3di  32525  tpssg  32604  eliccelico  32847  pmtrprfv2  33146  fzto1st  33161  psgnfzto1st  33163  qusker  33406  qusxpid  33420  lsmsnorb  33448  prmidl0  33507  mxidlirred  33529  ply1degltel  33651  ply1degleel  33652  eulerpartlemv  34505  eulerpartlemd  34507  eulerpartlemn  34522  prob01  34554  probun  34560  bnj170  34838  bnj248  34840  bnj252  34843  bnj253  34844  bnj945  34913  bnj1098  34923  bnj1224  34940  bnj150  35015  bnj153  35019  bnj545  35034  bnj557  35040  bnj571  35045  bnj594  35051  bnj864  35061  bnj865  35062  bnj849  35064  bnj964  35082  bnj986  35094  bnj996  35095  bnj1033  35108  bnj1110  35121  bnj1128  35129  bnj1174  35142  subgrwlk  35311  cusgr3cyclex  35315  loop1cycl  35316  2cycl2d  35318  pconnconn  35410  resconn  35425  iscvm  35438  cvmlift2lem12  35493  cvmlift3lem5  35502  satfdm  35548  elmpst  35715  mpstrcl  35720  lediv2aALT  35856  3jcadALT  35866  dfso3  35899  br6  35936  elfuns  36092  brimg  36114  lemsuccf  36118  cgrxfr  36234  segcon2  36284  seglecgr12im  36289  seglecgr12  36290  segletr  36293  btwnoutside  36304  broutsideof3  36305  outsideoftr  36308  outsidele  36311  bj-imn3ani  36849  relowlpssretop  37677  wl-df3-3mintru2  37799  lindsenlbs  37933  matunitlindflem2  37935  fdc  38063  isbnd3b  38103  ablo4pnp  38198  crngm4  38321  isidlc  38333  pridl  38355  ispridl2  38356  ispridlc  38388  ts3an1  38468  ts3an2  38469  ts3an3  38470  brres2  38591  disjressuc2  38729  xrninxp  38733  dfsuccl4  38792  dfeqvrels2  38990  dfeqvrel2  38992  dfeqvrel3  38993  dfeldisj3  39129  islshpsm  39423  islshpat  39460  cmtfvalN  39653  cmtvalN  39654  ishlat1  39795  ishlat2  39796  3dim0  39900  2dim  39913  islvol5  40022  lhpexle3  40455  cdleme0ex2N  40667  cdleme0nex  40733  cdlemg2cex  41034  cdlemg33b0  41144  cdlemg33b  41150  cdlemg33c  41151  cdlemg33e  41153  dib1dim  41608  diblsmopel  41614  dihopelvalcpre  41691  lcfls1c  41979  aks6d1c1p1  42543  aks6d1c1p1rcl  42544  sn-sup2  42933  sn-isghm  43103  3anrabdioph  43211  fgraphxp  43629  omge2  43723  faosnf0.11b  43851  dfsucon  43947  pren2  43977  dfrtrcl5  44053  brfvrcld2  44116  df3an2  44193  dfvd3  45015  3impexpVD  45279  modelaxreplem1  45402  rfcnnnub  45464  stoweidlem35  46460  smflimlem4  47199  ndmaovass  47645  nltle2tri  47752  elfz2z  47754  prproropf1olem0  47953  reuprpr  47974  gboge9  48231  sbgoldbalt  48248  nnsum4primesodd  48263  nnsum4primesoddALTV  48264  bgoldbtbndlem4  48275  bgoldbtbnd  48276  dfvopnbgr2  48320  isuspgrim  48363  isubgr3stgrlem7  48439  grlimprop2  48453  uhgrimgrlim  48454  pgn4cyclex  48593  rngcsectALTV  48742  rngcinvALTV  48743  ringcsectALTV  48776  ringcinvALTV  48777  islindeps  48920  islindeps2  48950  isldepslvec2  48952  elbigo2  49019  line2ylem  49218  io1ii  49387  catprsc  49479  0funcglem  49549  0funclem  49552  catcsect  49864  isthincd2  49903  thincsect  49933  2arwcatlem1  50061