Definition df-3an 1095

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

This definition is referenced by:  3anass  1101  3anan32  1103  3ancomb  1105  3anidm  1110  3an4anass  1111  3ioran  1112  3ianor  1113  3impa  1116  3expa  1125  3jca  1135  3anbi123i  1162  3pm3.2i  1347  3jaob  1435  3anbi123d  1445  3anim123d  1452  an6  1454  an3andi  1491  an33rean  1492  cadan  1617  19.26-3an  1880  nf3and  1906  nf3an  1909  4exdistr  1969  sb3an  2093  eeeanv  2360  mopick2  2643  r19.26-3  3102  r3al  3179  r3ex  3180  rexlimdvvva  3199  3reeanv  3214  ceqsex3v  3485  ceqsex4v  3486  ceqsex8v  3488  rspc4v  3581  sbc3an  3788  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  6780  2f1fvneq  7207  fpropnf1  7214  dff1o6  7222  oprabidw  7390  oprabid  7391  oprabv  7419  ndmovass  7547  elovmpo  7604  elovmporab  7605  elovmporab1w  7606  elovmporab1  7607  elovmpt3rab1  7619  dfwe2  7720  opiota  8003  dfxp3  8005  bropopvvv  8031  poxp2  8085  xpord2pred  8087  xpord3pred  8094  sexp3  8095  oaord  8476  oeeu  8533  nnaord  8549  naddasslem1  8624  swoso  8672  fiint  9231  funsnfsupp  9299  ttrclselem2  9642  alephval3  10027  ingru  10734  axgroth3  10750  ltrelxr  11202  ltxrlt  11212  wloglei  11678  sup2  12107  rexuz2  12844  ltxr  13061  elixx3g  13306  ixxun  13309  dfrp2  13342  elioo4g  13354  elioopnf  13391  elioomnf  13392  elicopnf  13393  elxrge0  13405  divelunit  13442  elfz2  13463  elfzuzb  13467  uzsplit  13545  fznn0  13568  elfzmlbp  13588  preduz  13599  elfzo2  13611  fzolb2  13616  fzouzsplit  13644  ssfzo12bi  13711  fzind2  13738  hashgt23el  14381  ccatsymb  14540  swrdsbslen  14622  swrdspsleq  14623  swrdccatin2  14686  pfxccatin12lem2  14688  pfxccatin12lem3  14689  pfxccatin12  14690  pfxccat3a  14695  repsdf2  14735  repswsymball  14736  repswsymballbi  14737  repswswrd  14741  s3eq3seq  14896  wrdl3s3  14919  s3sndisj  14924  s3iunsndisj  14925  abs2dif  15290  sinltx  16151  divalglem8  16364  divalglem10  16366  divalgb  16368  bitsval2  16389  divgcdz  16475  rplpwr  16522  cncongr1  16631  pythagtriplem2  16783  pythagtrip  16800  prmgaplem4  17020  isstruct  17117  setsstruct2  17139  imasvscafn  17496  xpscf  17524  mreexmrid  17604  iscatd2  17642  issect  17715  issect2  17716  oppcsect  17740  isfunc  17826  funcpropd  17864  fucsect  17937  fucinv  17938  initoeu2  17978  setcsect  18051  setcinv  18052  issgrpd  18693  ismhm0  18753  issubm2  18767  issubg3  19115  resgrpisgrp  19118  eqgval  19147  eqger  19148  cycsubgcl  19176  isgim  19231  gim0to0  19238  gaorb  19276  gaorber  19277  gastacos  19279  symg2bas  19362  galactghm  19373  pmtr3ncom  19444  ispgp  19561  efgcpbllema  19723  efgcpbllemb  19724  eqgabl  19803  qusecsub  19804  cygabl  19860  dprdw  19981  omndmul2  20102  rnglz  20140  rngpropd  20149  ringpropd  20263  ringrghm  20288  isirred2  20395  rngcsect  20611  rngcinv  20612  ringcsect  20645  ringcinv  20646  drngid2  20727  issdrg2  20770  isorng  20836  islss  20927  islmim  21055  lmhmpropd  21066  zndvds  21527  znleval  21532  znleval2  21533  obselocv  21706  mpfrcl  22064  matinvgcell  22421  mat1dimscm  22461  scmatscm  22499  scmatf1  22517  mdetunilem7  22604  cpmatacl  22702  cpmatmcl  22705  mat2pmatf1  22715  mat2pmatghm  22716  mat2pmatmul  22717  mat2pmatlin  22721  mat2pmatscmxcl  22726  m2pmfzgsumcl  22734  decpmataa0  22754  monmatcollpw  22765  pmatcollpwscmatlem1  22775  pmatcollpwscmatlem2  22776  pm2mpghm  22802  pm2mpmhmlem2  22805  monmat2matmon  22810  chfacfisf  22840  chfacfisfcpmat  22841  chfacfpmmulgsum2  22851  isbasis3g  22935  leordtvallem2  23197  lmfval  23218  lmbr  23244  lmbr2  23245  lmmo  23366  dfconn2  23405  ptbasin  23563  ptbasfi  23567  txcnpi  23594  ptcnp  23608  hausdiag  23631  qtophmeo  23803  fbunfip  23855  elflim2  23950  hausflimi  23966  isfcls  23995  isfcls2  23999  istmd  24060  istgp  24063  istrg  24150  istdrg  24152  istdrg2  24164  istlm  24171  imasdsf1olem  24359  xmeterval  24418  xmeter  24419  prdsxmslem2  24515  blval2  24548  isngp  24582  isngp2  24583  isngp3  24584  isnlm  24661  cnbl0  24759  cnblcld  24760  elii1  24923  isphtpc  24982  phtpcer  24983  isclmp  25085  iscph  25158  lmmbr  25246  lmmbr2  25247  lmmbrf  25250  iscfil2  25254  iscau3  25266  iscau4  25267  iscauf  25268  caucfil  25271  isbn  25326  ishl2  25358  ovolfcl  25454  ioombl1lem4  25549  mbfmax  25637  iblpos  25781  limcrcl  25862  ig1pval3  26164  ulmdvlem3  26388  ellogdm  26624  relogbcl  26758  fsumvma2  27198  chpchtsum  27203  chpub  27204  dchrelbas3  27222  gausslemma2dlem1a  27349  noetalem1  27725  sltssnb  27781  eqcuts  27797  eqcuts2  27798  lnhl  28703  colopp  28857  dfcgra2  28918  axeuclidlem  29051  axeuclid  29052  edgupgr  29223  umgr2edg1  29300  subusgr  29378  nbgrel  29429  nb3grpr2  29472  nb3gr2nb  29473  isuvtx  29484  nbupgruvtxres  29496  iscplgredg  29506  cplgr3v  29524  rusgrpropedg  29673  rgrusgrprc  29678  rusgrprc  29679  upgriswlk  29729  wlkonprop  29745  wksonproplem  29791  usgr2pth0  29853  isclwlke  29865  crctcshtrl  29911  iswwlksnx  29928  wwlknbp  29930  2trld  30026  rusgrnumwwlkl1  30059  rusgrnumwwlkb0  30062  rusgrnumwwlk  30066  clwlkclwwlkflem  30094  erclwwlkref  30110  clwwlkwwlksb  30144  erclwwlknref  30159  clwwlknon2x  30193  0wlk  30206  3spthd  30266  umgr3v3e3cycl  30274  frgr3v  30365  1to3vfriswmgr  30370  frgr2wwlkeu  30417  numclwwlk1lem2fo  30448  dlwwlknondlwlknonf1o  30455  nvex  30702  isnv  30703  dfadj2  31976  cnvadj  31983  adjeq  32026  eleigvec  32048  eleigvec2  32049  chirredi  32485  or3di  32548  tpssg  32627  eliccelico  32871  pmtrprfv2  33171  fzto1st  33186  psgnfzto1st  33188  qusker  33434  qusxpid  33448  lsmsnorb  33476  prmidl0  33535  mxidlirred  33557  ply1degltel  33687  ply1degleel  33688  eulerpartlemv  34558  eulerpartlemd  34560  eulerpartlemn  34575  prob01  34607  probun  34613  bnj170  34894  bnj248  34896  bnj252  34899  bnj253  34900  bnj945  34969  bnj1098  34979  bnj1224  34996  bnj150  35071  bnj153  35075  bnj545  35090  bnj557  35096  bnj571  35101  bnj594  35107  bnj864  35117  bnj865  35118  bnj849  35120  bnj964  35138  bnj986  35150  bnj996  35151  bnj1033  35164  bnj1110  35177  bnj1128  35185  bnj1174  35198  subgrwlk  35373  cusgr3cyclex  35377  loop1cycl  35378  2cycl2d  35380  pconnconn  35472  resconn  35487  iscvm  35500  cvmlift2lem12  35555  cvmlift3lem5  35564  satfdm  35610  elmpst  35777  mpstrcl  35782  lediv2aALT  35918  3jcadALT  35928  dfso3  35961  br6  35998  elfuns  36154  brimg  36176  lemsuccf  36180  cgrxfr  36296  segcon2  36346  seglecgr12im  36351  seglecgr12  36352  segletr  36355  btwnoutside  36366  broutsideof3  36367  outsideoftr  36370  outsidele  36373  bj-imn3ani  36911  relowlpssretop  37739  wl-df3-3mintru2  37861  lindsenlbs  37995  matunitlindflem2  37997  fdc  38125  isbnd3b  38165  ablo4pnp  38260  crngm4  38383  isidlc  38395  pridl  38417  ispridl2  38418  ispridlc  38450  ts3an1  38530  ts3an2  38531  ts3an3  38532  brres2  38653  disjressuc2  38791  xrninxp  38795  dfsuccl4  38854  dfeqvrels2  39052  dfeqvrel2  39054  dfeqvrel3  39055  dfeldisj3  39191  islshpsm  39485  islshpat  39522  cmtfvalN  39715  cmtvalN  39716  ishlat1  39857  ishlat2  39858  3dim0  39962  2dim  39975  islvol5  40084  lhpexle3  40517  cdleme0ex2N  40729  cdleme0nex  40795  cdlemg2cex  41096  cdlemg33b0  41206  cdlemg33b  41212  cdlemg33c  41213  cdlemg33e  41215  dib1dim  41670  diblsmopel  41676  dihopelvalcpre  41753  lcfls1c  42041  aks6d1c1p1  42605  aks6d1c1p1rcl  42606  sn-sup2  42994  sn-isghm  43136  3anrabdioph  43244  fgraphxp  43662  omge2  43756  faosnf0.11b  43884  dfsucon  43980  pren2  44010  dfrtrcl5  44086  brfvrcld2  44149  df3an2  44226  dfvd3  45048  3impexpVD  45312  modelaxreplem1  45435  rfcnnnub  45497  stoweidlem35  46490  smflimlem4  47229  ndmaovass  47681  nltle2tri  47788  elfz2z  47790  prproropf1olem0  47989  reuprpr  48010  gboge9  48267  sbgoldbalt  48284  nnsum4primesodd  48299  nnsum4primesoddALTV  48300  bgoldbtbndlem4  48311  bgoldbtbnd  48312  dfvopnbgr2  48356  isuspgrim  48399  isubgr3stgrlem7  48475  grlimprop2  48489  uhgrimgrlim  48490  pgn4cyclex  48629  rngcsectALTV  48778  rngcinvALTV  48779  ringcsectALTV  48812  ringcinvALTV  48813  islindeps  48956  islindeps2  48986  isldepslvec2  48988  elbigo2  49055  line2ylem  49254  io1ii  49423  catprsc  49515  0funcglem  49585  0funclem  49588  catcsect  49900  isthincd2  49939  thincsect  49969  2arwcatlem1  50097