Definition df-3an 1091

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 472. (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 1089	. 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒)
5	1, 2	wa 399	. . 3 wff (𝜑 ∧ 𝜓)
6	5, 3	wa 399	. 2 wff ((𝜑 ∧ 𝜓) ∧ 𝜒)
7	4, 6	wb 209	1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))

This definition is referenced by:  3anass  1097  3anan32  1099  3ancomb  1101  3anidm  1106  3an4anass  1107  3ioran  1108  3ianor  1109  3impa  1112  3expa  1120  3jca  1130  3anbi123i  1157  3pm3.2i  1341  3anbi123d  1438  3anim123d  1445  an6  1447  an3andi  1484  an33rean  1485  an33reanOLD  1486  cadan  1616  19.26-3an  1880  nf3and  1906  nf3an  1909  4exdistr  1970  sb3an  2089  eeeanv  2352  mopick2  2638  r19.26-3  3084  r3al  3113  3reeanv  3270  ceqsex3v  3450  ceqsex4v  3451  ceqsex8v  3453  sbc3an  3752  elin3  4100  rexdifpr  4560  raltpg  4600  tpss  4734  opthprneg  4761  dfopif  4766  dfopifOLD  4767  disjxun  5037  otth2  5352  otthg  5354  oteqex  5368  poirr  5465  po3nr  5468  wefrc  5530  rabxp  5582  f1orn  6649  fpropnf1  7057  dff1o6  7064  oprabidw  7222  oprabid  7223  oprabv  7249  ndmovass  7374  elovmpo  7428  elovmporab  7429  elovmporab1w  7430  elovmporab1  7431  elovmpt3rab1  7443  dfwe2  7537  opiota  7807  dfxp3  7809  bropopvvv  7836  oaord  8253  oeeu  8309  nnaord  8325  swoso  8402  fiint  8926  funsnfsupp  8987  alephval3  9689  ingru  10394  axgroth3  10410  ltrelxr  10859  ltxrlt  10868  wloglei  11329  sup2  11753  rexuz2  12460  ltxr  12672  elixx3g  12913  ixxun  12916  dfrp2  12949  elioo4g  12960  elioopnf  12996  elioomnf  12997  elicopnf  12998  elxrge0  13010  divelunit  13047  elfz2  13067  elfzuzb  13071  uzsplit  13149  fznn0  13169  elfzmlbp  13188  preduz  13199  elfzo2  13211  fzolb2  13215  fzouzsplit  13242  ssfzo12bi  13302  fzind2  13325  hashgt23el  13956  ccatsymb  14104  swrdsbslen  14194  swrdspsleq  14195  swrdccatin2  14259  pfxccatin12lem2  14261  pfxccatin12lem3  14262  pfxccatin12  14263  pfxccat3a  14268  repsdf2  14308  repswsymball  14309  repswsymballbi  14310  repswswrd  14314  s3eq3seq  14469  wrdl3s3  14494  s3sndisj  14495  s3iunsndisj  14496  abs2dif  14861  sinltx  15713  divalglem8  15924  divalglem10  15926  divalgb  15928  bitsval2  15947  divgcdz  16033  rplpwr  16082  cncongr1  16187  pythagtriplem2  16333  pythagtrip  16350  prmgaplem4  16570  isstruct  16679  setsstruct2  16703  imasvscafn  16996  xpscf  17024  mreexmrid  17100  iscatd2  17138  issect  17212  issect2  17213  oppcsect  17237  isfunc  17324  funcpropd  17361  fucsect  17435  fucinv  17436  initoeu2  17476  setcsect  17549  setcinv  17550  issubm2  18185  issubg3  18515  resgrpisgrp  18518  eqgval  18547  eqger  18548  cycsubgcl  18567  isgim  18620  gaorb  18655  gaorber  18656  gastacos  18658  symg2bas  18739  galactghm  18750  pmtr3ncom  18821  ispgp  18935  efgcpbllema  19098  efgcpbllemb  19099  eqgabl  19174  cygabl  19229  dprdw  19351  ringpropd  19554  ringrghm  19577  isirred2  19673  gim0to0  19716  drngid2  19737  issdrg2  19796  islss  19925  islmim  20053  lmhmpropd  20064  zndvds  20468  znleval  20473  znleval2  20474  obselocv  20644  isassa  20772  mpfrcl  20999  matinvgcell  21286  mat1dimscm  21326  scmatscm  21364  scmatf1  21382  mdetunilem7  21469  cpmatacl  21567  cpmatmcl  21570  mat2pmatf1  21580  mat2pmatghm  21581  mat2pmatmul  21582  mat2pmatlin  21586  mat2pmatscmxcl  21591  m2pmfzgsumcl  21599  decpmataa0  21619  monmatcollpw  21630  pmatcollpwscmatlem1  21640  pmatcollpwscmatlem2  21641  pm2mpghm  21667  pm2mpmhmlem2  21670  monmat2matmon  21675  chfacfisf  21705  chfacfisfcpmat  21706  chfacfpmmulgsum2  21716  isbasis3g  21800  leordtvallem2  22062  lmfval  22083  lmbr  22109  lmbr2  22110  lmmo  22231  dfconn2  22270  ptbasin  22428  ptbasfi  22432  txcnpi  22459  ptcnp  22473  hausdiag  22496  qtophmeo  22668  fbunfip  22720  elflim2  22815  hausflimi  22831  isfcls  22860  isfcls2  22864  istmd  22925  istgp  22928  istrg  23015  istdrg  23017  istdrg2  23029  istlm  23036  imasdsf1olem  23225  xmeterval  23284  xmeter  23285  prdsxmslem2  23381  blval2  23414  isngp  23448  isngp2  23449  isngp3  23450  isnlm  23527  cnbl0  23625  cnblcld  23626  elii1  23786  isphtpc  23845  phtpcer  23846  isclmp  23948  iscph  24021  lmmbr  24109  lmmbr2  24110  lmmbrf  24113  iscfil2  24117  iscau3  24129  iscau4  24130  iscauf  24131  caucfil  24134  isbn  24189  ishl2  24221  ovolfcl  24317  ioombl1lem4  24412  mbfmax  24500  iblpos  24644  limcrcl  24725  ig1pval3  25026  ulmdvlem3  25248  ellogdm  25481  relogbcl  25610  fsumvma2  26049  chpchtsum  26054  chpub  26055  dchrelbas3  26073  gausslemma2dlem1a  26200  lnhl  26660  colopp  26814  dfcgra2  26875  axeuclidlem  27007  axeuclid  27008  edgupgr  27179  umgr2edg1  27253  subusgr  27331  nbgrel  27382  nb3grpr2  27425  nb3gr2nb  27426  isuvtx  27437  nbupgruvtxres  27449  iscplgredg  27459  cplgr3v  27477  rusgrpropedg  27626  rgrusgrprc  27631  rusgrprc  27632  upgriswlk  27682  wlkonprop  27700  wksonproplem  27746  usgr2pth0  27806  isclwlke  27818  crctcshtrl  27861  iswwlksnx  27878  wwlknbp  27880  2trld  27976  rusgrnumwwlkl1  28006  rusgrnumwwlkb0  28009  rusgrnumwwlk  28013  clwlkclwwlkflem  28041  erclwwlkref  28057  clwwlkwwlksb  28091  erclwwlknref  28106  clwwlknon2x  28140  0wlk  28153  3spthd  28213  umgr3v3e3cycl  28221  frgr3v  28312  1to3vfriswmgr  28317  frgr2wwlkeu  28364  numclwwlk1lem2fo  28395  dlwwlknondlwlknonf1o  28402  nvex  28646  isnv  28647  dfadj2  29920  cnvadj  29927  adjeq  29970  eleigvec  29992  eleigvec2  29993  chirredi  30429  or3di  30483  eliccelico  30772  omndmul2  31011  pmtrprfv2  31030  fzto1st  31043  psgnfzto1st  31045  isorng  31171  qusker  31217  qusxpid  31227  lsmsnorb  31247  prmidl0  31294  eulerpartlemv  31997  eulerpartlemd  31999  eulerpartlemn  32014  prob01  32046  probun  32052  bnj170  32343  bnj248  32345  bnj252  32348  bnj253  32349  bnj945  32420  bnj1098  32430  bnj1224  32448  bnj150  32523  bnj153  32527  bnj545  32542  bnj557  32548  bnj571  32553  bnj594  32559  bnj864  32569  bnj865  32570  bnj849  32572  bnj964  32590  bnj986  32602  bnj996  32603  bnj1033  32616  bnj1110  32629  bnj1128  32637  bnj1174  32650  subgrwlk  32761  cusgr3cyclex  32765  loop1cycl  32766  2cycl2d  32768  pconnconn  32860  resconn  32875  iscvm  32888  cvmlift2lem12  32943  cvmlift3lem5  32952  satfdm  32998  elmpst  33165  mpstrcl  33170  lediv2aALT  33302  dfso3  33333  ot2elxp  33349  br6  33394  poxp2  33470  xpord2pred  33472  xpord3pred  33478  sexp3  33479  noetalem1  33630  eqscut  33685  eqscut2  33686  elfuns  33903  brimg  33925  brsuccf  33929  cgrxfr  34043  segcon2  34093  seglecgr12im  34098  seglecgr12  34099  segletr  34102  btwnoutside  34113  broutsideof3  34114  outsideoftr  34117  outsidele  34120  bj-imn3ani  34455  relowlpssretop  35221  wl-df3-3mintru2  35343  lindsenlbs  35458  matunitlindflem2  35460  fdc  35589  isbnd3b  35629  ablo4pnp  35724  crngm4  35847  isidlc  35859  pridl  35881  ispridl2  35882  ispridlc  35914  ts3an1  35994  ts3an2  35995  ts3an3  35996  brres2  36093  xrninxp  36204  dfeqvrels2  36387  dfeqvrel2  36389  dfeqvrel3  36390  dfeldisj3  36516  islshpsm  36680  islshpat  36717  cmtfvalN  36910  cmtvalN  36911  ishlat1  37052  ishlat2  37053  3dim0  37157  2dim  37170  islvol5  37279  lhpexle3  37712  cdleme0ex2N  37924  cdleme0nex  37990  cdlemg2cex  38291  cdlemg33b0  38401  cdlemg33b  38407  cdlemg33c  38408  cdlemg33e  38410  dib1dim  38865  diblsmopel  38871  dihopelvalcpre  38948  lcfls1c  39236  sn-sup2  40088  3anrabdioph  40248  fgraphxp  40680  dfsucon  40756  pren2  40777  dfrtrcl5  40854  brfvrcld2  40918  df3an2  40995  dfvd3  41825  3impexpVD  42090  rfcnnnub  42193  stoweidlem35  43194  smflimlem4  43924  ndmaovass  44313  nltle2tri  44421  elfz2z  44423  prproropf1olem0  44570  reuprpr  44591  gboge9  44832  sbgoldbalt  44849  nnsum4primesodd  44864  nnsum4primesoddALTV  44865  bgoldbtbndlem4  44876  bgoldbtbnd  44877  ismhm0  44975  rnglz  45058  rngcsect  45154  rngcinv  45155  rngcsectALTV  45166  rngcinvALTV  45167  ringcsect  45205  ringcinv  45206  ringcsectALTV  45229  ringcinvALTV  45230  islindeps  45410  islindeps2  45440  isldepslvec2  45442  elbigo2  45514  line2ylem  45713  io1ii  45830  catprsc  45910  isthincd2  45935  thincsect  45954