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  2353  mopick2  2636  r19.26-3  3096  r3al  3173  r3ex  3174  rexlimdvvva  3193  3reeanv  3208  ceqsex3v  3481  ceqsex4v  3482  ceqsex8v  3484  rspc4v  3582  sbc3an  3789  elin3  4137  rexdifpr  4593  raltpg  4632  tpss  4770  opthprneg  4798  dfopif  4803  disjxun  5072  otth2  5425  otthg  5427  oteqex  5443  poirr  5540  po3nr  5543  wefrc  5614  otelxp  5664  rabxp  5668  f1orn  6779  2f1fvneq  7204  fpropnf1  7211  dff1o6  7219  oprabidw  7387  oprabid  7388  oprabv  7416  ndmovass  7544  elovmpo  7601  elovmporab  7602  elovmporab1w  7603  elovmporab1  7604  elovmpt3rab1  7616  dfwe2  7717  opiota  8001  dfxp3  8003  bropopvvv  8029  poxp2  8082  xpord2pred  8084  xpord3pred  8091  sexp3  8092  oaord  8471  oeeu  8528  nnaord  8544  naddasslem1  8619  swoso  8667  fiint  9226  funsnfsupp  9294  ttrclselem2  9636  alephval3  10021  ingru  10727  axgroth3  10743  ltrelxr  11195  ltxrlt  11205  wloglei  11671  sup2  12101  rexuz2  12838  ltxr  13055  elixx3g  13300  ixxun  13303  dfrp2  13336  elioo4g  13348  elioopnf  13385  elioomnf  13386  elicopnf  13387  elxrge0  13399  divelunit  13436  elfz2  13457  elfzuzb  13461  uzsplit  13539  fznn0  13562  elfzmlbp  13582  preduz  13593  elfzo2  13605  fzolb2  13610  fzouzsplit  13638  ssfzo12bi  13705  fzind2  13732  hashgt23el  14375  ccatsymb  14534  swrdsbslen  14616  swrdspsleq  14617  swrdccatin2  14680  pfxccatin12lem2  14682  pfxccatin12lem3  14683  pfxccatin12  14684  pfxccat3a  14689  repsdf2  14729  repswsymball  14730  repswsymballbi  14731  repswswrd  14735  s3eq3seq  14890  wrdl3s3  14913  s3sndisj  14918  s3iunsndisj  14919  abs2dif  15284  sinltx  16145  divalglem8  16358  divalglem10  16360  divalgb  16362  bitsval2  16383  divgcdz  16469  rplpwr  16516  cncongr1  16625  pythagtriplem2  16777  pythagtrip  16794  prmgaplem4  17014  isstruct  17111  setsstruct2  17133  imasvscafn  17490  xpscf  17518  mreexmrid  17598  iscatd2  17636  issect  17709  issect2  17710  oppcsect  17734  isfunc  17820  funcpropd  17858  fucsect  17931  fucinv  17932  initoeu2  17972  setcsect  18045  setcinv  18046  issgrpd  18687  ismhm0  18747  issubm2  18761  issubg3  19109  resgrpisgrp  19112  eqgval  19141  eqger  19142  cycsubgcl  19170  isgim  19226  gim0to0  19233  gaorb  19271  gaorber  19272  gastacos  19274  symg2bas  19357  galactghm  19368  pmtr3ncom  19439  ispgp  19556  efgcpbllema  19718  efgcpbllemb  19719  eqgabl  19798  qusecsub  19799  cygabl  19855  dprdw  19976  omndmul2  20097  rnglz  20135  rngpropd  20144  ringpropd  20258  ringrghm  20283  isirred2  20390  rngcsect  20602  rngcinv  20603  ringcsect  20636  ringcinv  20637  drngid2  20718  issdrg2  20761  isorng  20827  islss  20918  islmim  21046  lmhmpropd  21057  zndvds  21518  znleval  21523  znleval2  21524  obselocv  21697  mpfrcl  22052  matinvgcell  22388  mat1dimscm  22428  scmatscm  22466  scmatf1  22484  mdetunilem7  22571  cpmatacl  22669  cpmatmcl  22672  mat2pmatf1  22682  mat2pmatghm  22683  mat2pmatmul  22684  mat2pmatlin  22688  mat2pmatscmxcl  22693  m2pmfzgsumcl  22701  decpmataa0  22721  monmatcollpw  22732  pmatcollpwscmatlem1  22742  pmatcollpwscmatlem2  22743  pm2mpghm  22769  pm2mpmhmlem2  22772  monmat2matmon  22777  chfacfisf  22807  chfacfisfcpmat  22808  chfacfpmmulgsum2  22818  isbasis3g  22902  leordtvallem2  23164  lmfval  23185  lmbr  23211  lmbr2  23212  lmmo  23333  dfconn2  23372  ptbasin  23530  ptbasfi  23534  txcnpi  23561  ptcnp  23575  hausdiag  23598  qtophmeo  23770  fbunfip  23822  elflim2  23917  hausflimi  23933  isfcls  23962  isfcls2  23966  istmd  24027  istgp  24030  istrg  24117  istdrg  24119  istdrg2  24131  istlm  24138  imasdsf1olem  24326  xmeterval  24385  xmeter  24386  prdsxmslem2  24482  blval2  24515  isngp  24549  isngp2  24550  isngp3  24551  isnlm  24628  cnbl0  24726  cnblcld  24727  elii1  24890  isphtpc  24949  phtpcer  24950  isclmp  25052  iscph  25125  lmmbr  25213  lmmbr2  25214  lmmbrf  25217  iscfil2  25221  iscau3  25233  iscau4  25234  iscauf  25235  caucfil  25238  isbn  25293  ishl2  25325  ovolfcl  25421  ioombl1lem4  25516  mbfmax  25604  iblpos  25748  limcrcl  25829  ig1pval3  26131  ulmdvlem3  26355  ellogdm  26591  relogbcl  26725  fsumvma2  27165  chpchtsum  27170  chpub  27171  dchrelbas3  27189  gausslemma2dlem1a  27316  noetalem1  27693  sltssnb  27749  eqcuts  27765  eqcuts2  27766  lnhl  28671  colopp  28825  dfcgra2  28886  axeuclidlem  29019  axeuclid  29020  edgupgr  29191  umgr2edg1  29268  subusgr  29346  nbgrel  29397  nb3grpr2  29440  nb3gr2nb  29441  isuvtx  29452  nbupgruvtxres  29464  iscplgredg  29474  cplgr3v  29492  rusgrpropedg  29641  rgrusgrprc  29646  rusgrprc  29647  upgriswlk  29697  wlkonprop  29713  wksonproplem  29759  usgr2pth0  29821  isclwlke  29833  crctcshtrl  29879  iswwlksnx  29896  wwlknbp  29898  2trld  29994  rusgrnumwwlkl1  30027  rusgrnumwwlkb0  30030  rusgrnumwwlk  30034  clwlkclwwlkflem  30062  erclwwlkref  30078  clwwlkwwlksb  30112  erclwwlknref  30127  clwwlknon2x  30161  0wlk  30174  3spthd  30234  umgr3v3e3cycl  30242  frgr3v  30333  1to3vfriswmgr  30338  frgr2wwlkeu  30385  numclwwlk1lem2fo  30416  dlwwlknondlwlknonf1o  30423  nvex  30670  isnv  30671  dfadj2  31944  cnvadj  31951  adjeq  31994  eleigvec  32016  eleigvec2  32017  chirredi  32453  or3di  32516  tpssg  32595  eliccelico  32838  pmtrprfv2  33137  fzto1st  33152  psgnfzto1st  33154  qusker  33397  qusxpid  33411  lsmsnorb  33439  prmidl0  33498  mxidlirred  33520  ply1degltel  33642  ply1degleel  33643  eulerpartlemv  34496  eulerpartlemd  34498  eulerpartlemn  34513  prob01  34545  probun  34551  bnj170  34829  bnj248  34831  bnj252  34834  bnj253  34835  bnj945  34904  bnj1098  34914  bnj1224  34931  bnj150  35006  bnj153  35010  bnj545  35025  bnj557  35031  bnj571  35036  bnj594  35042  bnj864  35052  bnj865  35053  bnj849  35055  bnj964  35073  bnj986  35085  bnj996  35086  bnj1033  35099  bnj1110  35112  bnj1128  35120  bnj1174  35133  subgrwlk  35302  cusgr3cyclex  35306  loop1cycl  35307  2cycl2d  35309  pconnconn  35401  resconn  35416  iscvm  35429  cvmlift2lem12  35484  cvmlift3lem5  35493  satfdm  35539  elmpst  35706  mpstrcl  35711  lediv2aALT  35847  3jcadALT  35857  dfso3  35890  br6  35927  elfuns  36083  brimg  36105  lemsuccf  36109  cgrxfr  36225  segcon2  36275  seglecgr12im  36280  seglecgr12  36281  segletr  36284  btwnoutside  36295  broutsideof3  36296  outsideoftr  36299  outsidele  36302  bj-imn3ani  36840  relowlpssretop  37668  wl-df3-3mintru2  37790  lindsenlbs  37924  matunitlindflem2  37926  fdc  38054  isbnd3b  38094  ablo4pnp  38189  crngm4  38312  isidlc  38324  pridl  38346  ispridl2  38347  ispridlc  38379  ts3an1  38459  ts3an2  38460  ts3an3  38461  brres2  38582  disjressuc2  38720  xrninxp  38724  dfsuccl4  38783  dfeqvrels2  38981  dfeqvrel2  38983  dfeqvrel3  38984  dfeldisj3  39120  islshpsm  39414  islshpat  39451  cmtfvalN  39644  cmtvalN  39645  ishlat1  39786  ishlat2  39787  3dim0  39891  2dim  39904  islvol5  40013  lhpexle3  40446  cdleme0ex2N  40658  cdleme0nex  40724  cdlemg2cex  41025  cdlemg33b0  41135  cdlemg33b  41141  cdlemg33c  41142  cdlemg33e  41144  dib1dim  41599  diblsmopel  41605  dihopelvalcpre  41682  lcfls1c  41970  aks6d1c1p1  42534  aks6d1c1p1rcl  42535  sn-sup2  42924  sn-isghm  43094  3anrabdioph  43202  fgraphxp  43620  omge2  43714  faosnf0.11b  43842  dfsucon  43938  pren2  43968  dfrtrcl5  44044  brfvrcld2  44107  df3an2  44184  dfvd3  45006  3impexpVD  45270  modelaxreplem1  45393  rfcnnnub  45455  stoweidlem35  46451  smflimlem4  47190  ndmaovass  47642  nltle2tri  47749  elfz2z  47751  prproropf1olem0  47950  reuprpr  47971  gboge9  48228  sbgoldbalt  48245  nnsum4primesodd  48260  nnsum4primesoddALTV  48261  bgoldbtbndlem4  48272  bgoldbtbnd  48273  dfvopnbgr2  48317  isuspgrim  48360  isubgr3stgrlem7  48436  grlimprop2  48450  uhgrimgrlim  48451  pgn4cyclex  48590  rngcsectALTV  48739  rngcinvALTV  48740  ringcsectALTV  48773  ringcinvALTV  48774  islindeps  48917  islindeps2  48947  isldepslvec2  48949  elbigo2  49016  line2ylem  49215  io1ii  49384  catprsc  49476  0funcglem  49546  0funclem  49549  catcsect  49861  isthincd2  49900  thincsect  49930  2arwcatlem1  50058