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  1610  19.26-3an  1873  nf3and  1899  nf3an  1902  4exdistr  1962  sb3an  2086  eeeanv  2352  mopick2  2634  r19.26-3  3094  r3al  3171  r3ex  3172  rexlimdvvva  3191  3reeanv  3206  ceqsex3v  3492  ceqsex4v  3493  ceqsex8v  3495  rspc4v  3593  sbc3an  3802  elin3  4155  rexdifpr  4611  raltpg  4650  tpss  4788  opthprneg  4816  dfopif  4821  disjxun  5091  otth2  5426  otthg  5428  oteqex  5443  poirr  5539  po3nr  5542  wefrc  5613  otelxp  5663  rabxp  5667  f1orn  6778  2f1fvneq  7200  fpropnf1  7207  dff1o6  7215  oprabidw  7383  oprabid  7384  oprabv  7412  ndmovass  7540  elovmpo  7597  elovmporab  7598  elovmporab1w  7599  elovmporab1  7600  elovmpt3rab1  7612  dfwe2  7713  opiota  7997  dfxp3  7999  bropopvvv  8026  poxp2  8079  xpord2pred  8081  xpord3pred  8088  sexp3  8089  oaord  8468  oeeu  8524  nnaord  8540  naddasslem1  8615  swoso  8662  fiint  9218  funsnfsupp  9283  ttrclselem2  9623  alephval3  10008  ingru  10713  axgroth3  10729  ltrelxr  11180  ltxrlt  11190  wloglei  11656  sup2  12085  rexuz2  12799  ltxr  13016  elixx3g  13260  ixxun  13263  dfrp2  13296  elioo4g  13308  elioopnf  13345  elioomnf  13346  elicopnf  13347  elxrge0  13359  divelunit  13396  elfz2  13416  elfzuzb  13420  uzsplit  13498  fznn0  13521  elfzmlbp  13541  preduz  13552  elfzo2  13564  fzolb2  13568  fzouzsplit  13596  ssfzo12bi  13663  fzind2  13690  hashgt23el  14333  ccatsymb  14492  swrdsbslen  14574  swrdspsleq  14575  swrdccatin2  14638  pfxccatin12lem2  14640  pfxccatin12lem3  14641  pfxccatin12  14642  pfxccat3a  14647  repsdf2  14687  repswsymball  14688  repswsymballbi  14689  repswswrd  14693  s3eq3seq  14848  wrdl3s3  14871  s3sndisj  14876  s3iunsndisj  14877  abs2dif  15242  sinltx  16100  divalglem8  16313  divalglem10  16315  divalgb  16317  bitsval2  16338  divgcdz  16424  rplpwr  16471  cncongr1  16580  pythagtriplem2  16731  pythagtrip  16748  prmgaplem4  16968  isstruct  17065  setsstruct2  17087  imasvscafn  17443  xpscf  17471  mreexmrid  17551  iscatd2  17589  issect  17662  issect2  17663  oppcsect  17687  isfunc  17773  funcpropd  17811  fucsect  17884  fucinv  17885  initoeu2  17925  setcsect  17998  setcinv  17999  issgrpd  18640  ismhm0  18700  issubm2  18714  issubg3  19059  resgrpisgrp  19062  eqgval  19091  eqger  19092  cycsubgcl  19120  isgim  19176  gim0to0  19183  gaorb  19221  gaorber  19222  gastacos  19224  symg2bas  19307  galactghm  19318  pmtr3ncom  19389  ispgp  19506  efgcpbllema  19668  efgcpbllemb  19669  eqgabl  19748  qusecsub  19749  cygabl  19805  dprdw  19926  omndmul2  20047  rnglz  20085  rngpropd  20094  ringpropd  20208  ringrghm  20233  isirred2  20341  rngcsect  20553  rngcinv  20554  ringcsect  20587  ringcinv  20588  drngid2  20669  issdrg2  20712  isorng  20778  islss  20869  islmim  20998  lmhmpropd  21009  zndvds  21488  znleval  21493  znleval2  21494  obselocv  21667  mpfrcl  22021  matinvgcell  22351  mat1dimscm  22391  scmatscm  22429  scmatf1  22447  mdetunilem7  22534  cpmatacl  22632  cpmatmcl  22635  mat2pmatf1  22645  mat2pmatghm  22646  mat2pmatmul  22647  mat2pmatlin  22651  mat2pmatscmxcl  22656  m2pmfzgsumcl  22664  decpmataa0  22684  monmatcollpw  22695  pmatcollpwscmatlem1  22705  pmatcollpwscmatlem2  22706  pm2mpghm  22732  pm2mpmhmlem2  22735  monmat2matmon  22740  chfacfisf  22770  chfacfisfcpmat  22771  chfacfpmmulgsum2  22781  isbasis3g  22865  leordtvallem2  23127  lmfval  23148  lmbr  23174  lmbr2  23175  lmmo  23296  dfconn2  23335  ptbasin  23493  ptbasfi  23497  txcnpi  23524  ptcnp  23538  hausdiag  23561  qtophmeo  23733  fbunfip  23785  elflim2  23880  hausflimi  23896  isfcls  23925  isfcls2  23929  istmd  23990  istgp  23993  istrg  24080  istdrg  24082  istdrg2  24094  istlm  24101  imasdsf1olem  24289  xmeterval  24348  xmeter  24349  prdsxmslem2  24445  blval2  24478  isngp  24512  isngp2  24513  isngp3  24514  isnlm  24591  cnbl0  24689  cnblcld  24690  elii1  24859  isphtpc  24921  phtpcer  24922  isclmp  25025  iscph  25098  lmmbr  25186  lmmbr2  25187  lmmbrf  25190  iscfil2  25194  iscau3  25206  iscau4  25207  iscauf  25208  caucfil  25211  isbn  25266  ishl2  25298  ovolfcl  25395  ioombl1lem4  25490  mbfmax  25578  iblpos  25722  limcrcl  25803  ig1pval3  26111  ulmdvlem3  26339  ellogdm  26576  relogbcl  26711  fsumvma2  27153  chpchtsum  27158  chpub  27159  dchrelbas3  27177  gausslemma2dlem1a  27304  noetalem1  27681  ssltsnb  27733  eqscut  27747  eqscut2  27748  lnhl  28594  colopp  28748  dfcgra2  28809  axeuclidlem  28942  axeuclid  28943  edgupgr  29114  umgr2edg1  29191  subusgr  29269  nbgrel  29320  nb3grpr2  29363  nb3gr2nb  29364  isuvtx  29375  nbupgruvtxres  29387  iscplgredg  29397  cplgr3v  29415  rusgrpropedg  29565  rgrusgrprc  29570  rusgrprc  29571  upgriswlk  29621  wlkonprop  29637  wksonproplem  29683  usgr2pth0  29745  isclwlke  29757  crctcshtrl  29803  iswwlksnx  29820  wwlknbp  29822  2trld  29918  rusgrnumwwlkl1  29951  rusgrnumwwlkb0  29954  rusgrnumwwlk  29958  clwlkclwwlkflem  29986  erclwwlkref  30002  clwwlkwwlksb  30036  erclwwlknref  30051  clwwlknon2x  30085  0wlk  30098  3spthd  30158  umgr3v3e3cycl  30166  frgr3v  30257  1to3vfriswmgr  30262  frgr2wwlkeu  30309  numclwwlk1lem2fo  30340  dlwwlknondlwlknonf1o  30347  nvex  30593  isnv  30594  dfadj2  31867  cnvadj  31874  adjeq  31917  eleigvec  31939  eleigvec2  31940  chirredi  32376  or3di  32440  tpssg  32519  eliccelico  32764  pmtrprfv2  33064  fzto1st  33079  psgnfzto1st  33081  qusker  33321  qusxpid  33335  lsmsnorb  33363  prmidl0  33422  mxidlirred  33444  ply1degltel  33562  ply1degleel  33563  eulerpartlemv  34398  eulerpartlemd  34400  eulerpartlemn  34415  prob01  34447  probun  34453  bnj170  34731  bnj248  34733  bnj252  34736  bnj253  34737  bnj945  34806  bnj1098  34816  bnj1224  34834  bnj150  34909  bnj153  34913  bnj545  34928  bnj557  34934  bnj571  34939  bnj594  34945  bnj864  34955  bnj865  34956  bnj849  34958  bnj964  34976  bnj986  34988  bnj996  34989  bnj1033  35002  bnj1110  35015  bnj1128  35023  bnj1174  35036  subgrwlk  35197  cusgr3cyclex  35201  loop1cycl  35202  2cycl2d  35204  pconnconn  35296  resconn  35311  iscvm  35324  cvmlift2lem12  35379  cvmlift3lem5  35388  satfdm  35434  elmpst  35601  mpstrcl  35606  lediv2aALT  35742  3jcadALT  35752  dfso3  35785  br6  35822  elfuns  35978  brimg  36000  lemsuccf  36004  cgrxfr  36120  segcon2  36170  seglecgr12im  36175  seglecgr12  36176  segletr  36179  btwnoutside  36190  broutsideof3  36191  outsideoftr  36194  outsidele  36197  bj-imn3ani  36652  relowlpssretop  37429  wl-df3-3mintru2  37551  lindsenlbs  37675  matunitlindflem2  37677  fdc  37805  isbnd3b  37845  ablo4pnp  37940  crngm4  38063  isidlc  38075  pridl  38097  ispridl2  38098  ispridlc  38130  ts3an1  38210  ts3an2  38211  ts3an3  38212  brres2  38325  disjressuc2  38455  xrninxp  38459  dfsuccl4  38507  dfeqvrels2  38704  dfeqvrel2  38706  dfeqvrel3  38707  dfeldisj3  38837  islshpsm  39099  islshpat  39136  cmtfvalN  39329  cmtvalN  39330  ishlat1  39471  ishlat2  39472  3dim0  39576  2dim  39589  islvol5  39698  lhpexle3  40131  cdleme0ex2N  40343  cdleme0nex  40409  cdlemg2cex  40710  cdlemg33b0  40820  cdlemg33b  40826  cdlemg33c  40827  cdlemg33e  40829  dib1dim  41284  diblsmopel  41290  dihopelvalcpre  41367  lcfls1c  41655  aks6d1c1p1  42220  aks6d1c1p1rcl  42221  sn-sup2  42609  sn-isghm  42791  3anrabdioph  42899  fgraphxp  43321  omge2  43415  faosnf0.11b  43544  dfsucon  43640  pren2  43670  dfrtrcl5  43746  brfvrcld2  43809  df3an2  43886  dfvd3  44708  3impexpVD  44972  modelaxreplem1  45095  rfcnnnub  45157  stoweidlem35  46157  smflimlem4  46896  ndmaovass  47330  nltle2tri  47437  elfz2z  47439  prproropf1olem0  47626  reuprpr  47647  gboge9  47888  sbgoldbalt  47905  nnsum4primesodd  47920  nnsum4primesoddALTV  47921  bgoldbtbndlem4  47932  bgoldbtbnd  47933  dfvopnbgr2  47977  isuspgrim  48020  isubgr3stgrlem7  48096  grlimprop2  48110  uhgrimgrlim  48111  pgn4cyclex  48250  rngcsectALTV  48399  rngcinvALTV  48400  ringcsectALTV  48433  ringcinvALTV  48434  islindeps  48578  islindeps2  48608  isldepslvec2  48610  elbigo2  48677  line2ylem  48876  io1ii  49045  catprsc  49138  0funcglem  49208  0funclem  49211  catcsect  49523  isthincd2  49562  thincsect  49592  2arwcatlem1  49720