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  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  2081  eeeanv  2352  mopick2  2637  r19.26-3  3112  r3al  3197  r3ex  3198  rexlimdvvva  3214  3reeanv  3230  ceqsex3v  3537  ceqsex4v  3538  ceqsex8v  3540  rspc4v  3642  sbc3an  3855  elin3  4206  rexdifpr  4659  raltpg  4698  tpss  4837  opthprneg  4865  dfopif  4870  disjxun  5141  otth2  5488  otthg  5490  oteqex  5505  poirr  5604  po3nr  5607  wefrc  5679  otelxp  5729  rabxp  5733  f1orn  6858  fpropnf1  7287  dff1o6  7295  oprabidw  7462  oprabid  7463  oprabv  7493  ndmovass  7621  elovmpo  7678  elovmporab  7679  elovmporab1w  7680  elovmporab1  7681  elovmpt3rab1  7693  dfwe2  7794  opiota  8084  dfxp3  8086  bropopvvv  8115  poxp2  8168  xpord2pred  8170  xpord3pred  8177  sexp3  8178  oaord  8585  oeeu  8641  nnaord  8657  naddasslem1  8732  swoso  8779  fiint  9366  fiintOLD  9367  funsnfsupp  9432  ttrclselem2  9766  alephval3  10150  ingru  10855  axgroth3  10871  ltrelxr  11322  ltxrlt  11331  wloglei  11795  sup2  12224  rexuz2  12941  ltxr  13157  elixx3g  13400  ixxun  13403  dfrp2  13436  elioo4g  13447  elioopnf  13483  elioomnf  13484  elicopnf  13485  elxrge0  13497  divelunit  13534  elfz2  13554  elfzuzb  13558  uzsplit  13636  fznn0  13659  elfzmlbp  13679  preduz  13690  elfzo2  13702  fzolb2  13706  fzouzsplit  13734  ssfzo12bi  13800  fzind2  13824  hashgt23el  14463  ccatsymb  14620  swrdsbslen  14702  swrdspsleq  14703  swrdccatin2  14767  pfxccatin12lem2  14769  pfxccatin12lem3  14770  pfxccatin12  14771  pfxccat3a  14776  repsdf2  14816  repswsymball  14817  repswsymballbi  14818  repswswrd  14822  s3eq3seq  14978  wrdl3s3  15001  s3sndisj  15006  s3iunsndisj  15007  abs2dif  15371  sinltx  16225  divalglem8  16437  divalglem10  16439  divalgb  16441  bitsval2  16462  divgcdz  16548  rplpwr  16595  cncongr1  16704  pythagtriplem2  16855  pythagtrip  16872  prmgaplem4  17092  isstruct  17189  setsstruct2  17211  imasvscafn  17582  xpscf  17610  mreexmrid  17686  iscatd2  17724  issect  17797  issect2  17798  oppcsect  17822  isfunc  17909  funcpropd  17947  fucsect  18020  fucinv  18021  initoeu2  18061  setcsect  18134  setcinv  18135  issgrpd  18743  ismhm0  18803  issubm2  18817  issubg3  19162  resgrpisgrp  19165  eqgval  19195  eqger  19196  cycsubgcl  19224  isgim  19280  gim0to0  19287  gaorb  19325  gaorber  19326  gastacos  19328  symg2bas  19410  galactghm  19422  pmtr3ncom  19493  ispgp  19610  efgcpbllema  19772  efgcpbllemb  19773  eqgabl  19852  qusecsub  19853  cygabl  19909  dprdw  20030  rnglz  20162  rngpropd  20171  ringpropd  20285  ringrghm  20310  isirred2  20421  rngcsect  20636  rngcinv  20637  ringcsect  20670  ringcinv  20671  drngid2  20752  issdrg2  20796  islss  20932  islmim  21061  lmhmpropd  21072  zndvds  21568  znleval  21573  znleval2  21574  obselocv  21748  mpfrcl  22109  matinvgcell  22441  mat1dimscm  22481  scmatscm  22519  scmatf1  22537  mdetunilem7  22624  cpmatacl  22722  cpmatmcl  22725  mat2pmatf1  22735  mat2pmatghm  22736  mat2pmatmul  22737  mat2pmatlin  22741  mat2pmatscmxcl  22746  m2pmfzgsumcl  22754  decpmataa0  22774  monmatcollpw  22785  pmatcollpwscmatlem1  22795  pmatcollpwscmatlem2  22796  pm2mpghm  22822  pm2mpmhmlem2  22825  monmat2matmon  22830  chfacfisf  22860  chfacfisfcpmat  22861  chfacfpmmulgsum2  22871  isbasis3g  22956  leordtvallem2  23219  lmfval  23240  lmbr  23266  lmbr2  23267  lmmo  23388  dfconn2  23427  ptbasin  23585  ptbasfi  23589  txcnpi  23616  ptcnp  23630  hausdiag  23653  qtophmeo  23825  fbunfip  23877  elflim2  23972  hausflimi  23988  isfcls  24017  isfcls2  24021  istmd  24082  istgp  24085  istrg  24172  istdrg  24174  istdrg2  24186  istlm  24193  imasdsf1olem  24383  xmeterval  24442  xmeter  24443  prdsxmslem2  24542  blval2  24575  isngp  24609  isngp2  24610  isngp3  24611  isnlm  24696  cnbl0  24794  cnblcld  24795  elii1  24964  isphtpc  25026  phtpcer  25027  isclmp  25130  iscph  25204  lmmbr  25292  lmmbr2  25293  lmmbrf  25296  iscfil2  25300  iscau3  25312  iscau4  25313  iscauf  25314  caucfil  25317  isbn  25372  ishl2  25404  ovolfcl  25501  ioombl1lem4  25596  mbfmax  25684  iblpos  25828  limcrcl  25909  ig1pval3  26217  ulmdvlem3  26445  ellogdm  26681  relogbcl  26816  fsumvma2  27258  chpchtsum  27263  chpub  27264  dchrelbas3  27282  gausslemma2dlem1a  27409  noetalem1  27786  eqscut  27850  eqscut2  27851  lnhl  28623  colopp  28777  dfcgra2  28838  axeuclidlem  28977  axeuclid  28978  edgupgr  29151  umgr2edg1  29228  subusgr  29306  nbgrel  29357  nb3grpr2  29400  nb3gr2nb  29401  isuvtx  29412  nbupgruvtxres  29424  iscplgredg  29434  cplgr3v  29452  rusgrpropedg  29602  rgrusgrprc  29607  rusgrprc  29608  upgriswlk  29659  wlkonprop  29676  wksonproplem  29722  wksonproplemOLD  29723  usgr2pth0  29785  isclwlke  29797  crctcshtrl  29843  iswwlksnx  29860  wwlknbp  29862  2trld  29958  rusgrnumwwlkl1  29988  rusgrnumwwlkb0  29991  rusgrnumwwlk  29995  clwlkclwwlkflem  30023  erclwwlkref  30039  clwwlkwwlksb  30073  erclwwlknref  30088  clwwlknon2x  30122  0wlk  30135  3spthd  30195  umgr3v3e3cycl  30203  frgr3v  30294  1to3vfriswmgr  30299  frgr2wwlkeu  30346  numclwwlk1lem2fo  30377  dlwwlknondlwlknonf1o  30384  nvex  30630  isnv  30631  dfadj2  31904  cnvadj  31911  adjeq  31954  eleigvec  31976  eleigvec2  31977  chirredi  32413  or3di  32478  eliccelico  32779  omndmul2  33089  pmtrprfv2  33108  fzto1st  33123  psgnfzto1st  33125  isorng  33329  qusker  33377  qusxpid  33391  lsmsnorb  33419  prmidl0  33478  mxidlirred  33500  ply1degltel  33615  ply1degleel  33616  eulerpartlemv  34366  eulerpartlemd  34368  eulerpartlemn  34383  prob01  34415  probun  34421  bnj170  34712  bnj248  34714  bnj252  34717  bnj253  34718  bnj945  34787  bnj1098  34797  bnj1224  34815  bnj150  34890  bnj153  34894  bnj545  34909  bnj557  34915  bnj571  34920  bnj594  34926  bnj864  34936  bnj865  34937  bnj849  34939  bnj964  34957  bnj986  34969  bnj996  34970  bnj1033  34983  bnj1110  34996  bnj1128  35004  bnj1174  35017  subgrwlk  35137  cusgr3cyclex  35141  loop1cycl  35142  2cycl2d  35144  pconnconn  35236  resconn  35251  iscvm  35264  cvmlift2lem12  35319  cvmlift3lem5  35328  satfdm  35374  elmpst  35541  mpstrcl  35546  lediv2aALT  35682  3jcadALT  35692  dfso3  35720  br6  35757  elfuns  35916  brimg  35938  brsuccf  35942  cgrxfr  36056  segcon2  36106  seglecgr12im  36111  seglecgr12  36112  segletr  36115  btwnoutside  36126  broutsideof3  36127  outsideoftr  36130  outsidele  36133  bj-imn3ani  36588  relowlpssretop  37365  wl-df3-3mintru2  37487  lindsenlbs  37622  matunitlindflem2  37624  fdc  37752  isbnd3b  37792  ablo4pnp  37887  crngm4  38010  isidlc  38022  pridl  38044  ispridl2  38045  ispridlc  38077  ts3an1  38157  ts3an2  38158  ts3an3  38159  brres2  38269  disjressuc2  38389  xrninxp  38393  dfeqvrels2  38589  dfeqvrel2  38591  dfeqvrel3  38592  dfeldisj3  38720  islshpsm  38981  islshpat  39018  cmtfvalN  39211  cmtvalN  39212  ishlat1  39353  ishlat2  39354  3dim0  39459  2dim  39472  islvol5  39581  lhpexle3  40014  cdleme0ex2N  40226  cdleme0nex  40292  cdlemg2cex  40593  cdlemg33b0  40703  cdlemg33b  40709  cdlemg33c  40710  cdlemg33e  40712  dib1dim  41167  diblsmopel  41173  dihopelvalcpre  41250  lcfls1c  41538  aks6d1c1p1  42108  aks6d1c1p1rcl  42109  sn-sup2  42501  sn-isghm  42683  3anrabdioph  42793  fgraphxp  43216  omge2  43311  faosnf0.11b  43440  dfsucon  43536  pren2  43566  dfrtrcl5  43642  brfvrcld2  43705  df3an2  43782  dfvd3  44611  3impexpVD  44876  modelaxreplem1  44995  rfcnnnub  45041  stoweidlem35  46050  smflimlem4  46789  ndmaovass  47218  nltle2tri  47325  elfz2z  47327  prproropf1olem0  47489  reuprpr  47510  gboge9  47751  sbgoldbalt  47768  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  bgoldbtbndlem4  47795  bgoldbtbnd  47796  dfvopnbgr2  47839  isubgr3stgrlem7  47939  grlimprop2  47953  uhgrimgrlim  47954  rngcsectALTV  48191  rngcinvALTV  48192  ringcsectALTV  48225  ringcinvALTV  48226  islindeps  48370  islindeps2  48400  isldepslvec2  48402  elbigo2  48473  line2ylem  48672  io1ii  48818  catprsc  48902  0funcglem  48916  0funclem  48919  isthincd2  49086  thincsect  49114