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  1609  19.26-3an  1872  nf3and  1898  nf3an  1901  4exdistr  1961  sb3an  2082  eeeanv  2348  mopick2  2630  r19.26-3  3090  r3al  3167  r3ex  3168  rexlimdvvva  3187  3reeanv  3202  ceqsex3v  3492  ceqsex4v  3493  ceqsex8v  3495  rspc4v  3597  sbc3an  3807  elin3  4157  rexdifpr  4611  raltpg  4650  tpss  4788  opthprneg  4816  dfopif  4821  disjxun  5090  otth2  5426  otthg  5428  oteqex  5443  poirr  5539  po3nr  5542  wefrc  5613  otelxp  5663  rabxp  5667  f1orn  6774  2f1fvneq  7197  fpropnf1  7204  dff1o6  7212  oprabidw  7380  oprabid  7381  oprabv  7409  ndmovass  7537  elovmpo  7594  elovmporab  7595  elovmporab1w  7596  elovmporab1  7597  elovmpt3rab1  7609  dfwe2  7710  opiota  7994  dfxp3  7996  bropopvvv  8023  poxp2  8076  xpord2pred  8078  xpord3pred  8085  sexp3  8086  oaord  8465  oeeu  8521  nnaord  8537  naddasslem1  8612  swoso  8659  fiint  9216  fiintOLD  9217  funsnfsupp  9282  ttrclselem2  9622  alephval3  10004  ingru  10709  axgroth3  10725  ltrelxr  11176  ltxrlt  11186  wloglei  11652  sup2  12081  rexuz2  12800  ltxr  13017  elixx3g  13261  ixxun  13264  dfrp2  13297  elioo4g  13309  elioopnf  13346  elioomnf  13347  elicopnf  13348  elxrge0  13360  divelunit  13397  elfz2  13417  elfzuzb  13421  uzsplit  13499  fznn0  13522  elfzmlbp  13542  preduz  13553  elfzo2  13565  fzolb2  13569  fzouzsplit  13597  ssfzo12bi  13664  fzind2  13688  hashgt23el  14331  ccatsymb  14489  swrdsbslen  14571  swrdspsleq  14572  swrdccatin2  14635  pfxccatin12lem2  14637  pfxccatin12lem3  14638  pfxccatin12  14639  pfxccat3a  14644  repsdf2  14684  repswsymball  14685  repswsymballbi  14686  repswswrd  14690  s3eq3seq  14846  wrdl3s3  14869  s3sndisj  14874  s3iunsndisj  14875  abs2dif  15240  sinltx  16098  divalglem8  16311  divalglem10  16313  divalgb  16315  bitsval2  16336  divgcdz  16422  rplpwr  16469  cncongr1  16578  pythagtriplem2  16729  pythagtrip  16746  prmgaplem4  16966  isstruct  17063  setsstruct2  17085  imasvscafn  17441  xpscf  17469  mreexmrid  17549  iscatd2  17587  issect  17660  issect2  17661  oppcsect  17685  isfunc  17771  funcpropd  17809  fucsect  17882  fucinv  17883  initoeu2  17923  setcsect  17996  setcinv  17997  issgrpd  18604  ismhm0  18664  issubm2  18678  issubg3  19023  resgrpisgrp  19026  eqgval  19056  eqger  19057  cycsubgcl  19085  isgim  19141  gim0to0  19148  gaorb  19186  gaorber  19187  gastacos  19189  symg2bas  19272  galactghm  19283  pmtr3ncom  19354  ispgp  19471  efgcpbllema  19633  efgcpbllemb  19634  eqgabl  19713  qusecsub  19714  cygabl  19770  dprdw  19891  omndmul2  20012  rnglz  20050  rngpropd  20059  ringpropd  20173  ringrghm  20198  isirred2  20306  rngcsect  20521  rngcinv  20522  ringcsect  20555  ringcinv  20556  drngid2  20637  issdrg2  20680  isorng  20746  islss  20837  islmim  20966  lmhmpropd  20977  zndvds  21456  znleval  21461  znleval2  21462  obselocv  21635  mpfrcl  21990  matinvgcell  22320  mat1dimscm  22360  scmatscm  22398  scmatf1  22416  mdetunilem7  22503  cpmatacl  22601  cpmatmcl  22604  mat2pmatf1  22614  mat2pmatghm  22615  mat2pmatmul  22616  mat2pmatlin  22620  mat2pmatscmxcl  22625  m2pmfzgsumcl  22633  decpmataa0  22653  monmatcollpw  22664  pmatcollpwscmatlem1  22674  pmatcollpwscmatlem2  22675  pm2mpghm  22701  pm2mpmhmlem2  22704  monmat2matmon  22709  chfacfisf  22739  chfacfisfcpmat  22740  chfacfpmmulgsum2  22750  isbasis3g  22834  leordtvallem2  23096  lmfval  23117  lmbr  23143  lmbr2  23144  lmmo  23265  dfconn2  23304  ptbasin  23462  ptbasfi  23466  txcnpi  23493  ptcnp  23507  hausdiag  23530  qtophmeo  23702  fbunfip  23754  elflim2  23849  hausflimi  23865  isfcls  23894  isfcls2  23898  istmd  23959  istgp  23962  istrg  24049  istdrg  24051  istdrg2  24063  istlm  24070  imasdsf1olem  24259  xmeterval  24318  xmeter  24319  prdsxmslem2  24415  blval2  24448  isngp  24482  isngp2  24483  isngp3  24484  isnlm  24561  cnbl0  24659  cnblcld  24660  elii1  24829  isphtpc  24891  phtpcer  24892  isclmp  24995  iscph  25068  lmmbr  25156  lmmbr2  25157  lmmbrf  25160  iscfil2  25164  iscau3  25176  iscau4  25177  iscauf  25178  caucfil  25181  isbn  25236  ishl2  25268  ovolfcl  25365  ioombl1lem4  25460  mbfmax  25548  iblpos  25692  limcrcl  25773  ig1pval3  26081  ulmdvlem3  26309  ellogdm  26546  relogbcl  26681  fsumvma2  27123  chpchtsum  27128  chpub  27129  dchrelbas3  27147  gausslemma2dlem1a  27274  noetalem1  27651  ssltsnb  27703  eqscut  27717  eqscut2  27718  lnhl  28564  colopp  28718  dfcgra2  28779  axeuclidlem  28911  axeuclid  28912  edgupgr  29083  umgr2edg1  29160  subusgr  29238  nbgrel  29289  nb3grpr2  29332  nb3gr2nb  29333  isuvtx  29344  nbupgruvtxres  29356  iscplgredg  29366  cplgr3v  29384  rusgrpropedg  29534  rgrusgrprc  29539  rusgrprc  29540  upgriswlk  29590  wlkonprop  29606  wksonproplem  29652  usgr2pth0  29714  isclwlke  29726  crctcshtrl  29772  iswwlksnx  29789  wwlknbp  29791  2trld  29887  rusgrnumwwlkl1  29917  rusgrnumwwlkb0  29920  rusgrnumwwlk  29924  clwlkclwwlkflem  29952  erclwwlkref  29968  clwwlkwwlksb  30002  erclwwlknref  30017  clwwlknon2x  30051  0wlk  30064  3spthd  30124  umgr3v3e3cycl  30132  frgr3v  30223  1to3vfriswmgr  30228  frgr2wwlkeu  30275  numclwwlk1lem2fo  30306  dlwwlknondlwlknonf1o  30313  nvex  30559  isnv  30560  dfadj2  31833  cnvadj  31840  adjeq  31883  eleigvec  31905  eleigvec2  31906  chirredi  32342  or3di  32407  tpssg  32486  eliccelico  32729  pmtrprfv2  33039  fzto1st  33054  psgnfzto1st  33056  qusker  33295  qusxpid  33309  lsmsnorb  33337  prmidl0  33396  mxidlirred  33418  ply1degltel  33536  ply1degleel  33537  eulerpartlemv  34348  eulerpartlemd  34350  eulerpartlemn  34365  prob01  34397  probun  34403  bnj170  34681  bnj248  34683  bnj252  34686  bnj253  34687  bnj945  34756  bnj1098  34766  bnj1224  34784  bnj150  34859  bnj153  34863  bnj545  34878  bnj557  34884  bnj571  34889  bnj594  34895  bnj864  34905  bnj865  34906  bnj849  34908  bnj964  34926  bnj986  34938  bnj996  34939  bnj1033  34952  bnj1110  34965  bnj1128  34973  bnj1174  34986  subgrwlk  35125  cusgr3cyclex  35129  loop1cycl  35130  2cycl2d  35132  pconnconn  35224  resconn  35239  iscvm  35252  cvmlift2lem12  35307  cvmlift3lem5  35316  satfdm  35362  elmpst  35529  mpstrcl  35534  lediv2aALT  35670  3jcadALT  35680  dfso3  35713  br6  35750  elfuns  35909  brimg  35931  brsuccf  35935  cgrxfr  36049  segcon2  36099  seglecgr12im  36104  seglecgr12  36105  segletr  36108  btwnoutside  36119  broutsideof3  36120  outsideoftr  36123  outsidele  36126  bj-imn3ani  36581  relowlpssretop  37358  wl-df3-3mintru2  37480  lindsenlbs  37615  matunitlindflem2  37617  fdc  37745  isbnd3b  37785  ablo4pnp  37880  crngm4  38003  isidlc  38015  pridl  38037  ispridl2  38038  ispridlc  38070  ts3an1  38150  ts3an2  38151  ts3an3  38152  brres2  38263  disjressuc2  38380  xrninxp  38384  dfeqvrels2  38585  dfeqvrel2  38587  dfeqvrel3  38588  dfeldisj3  38717  islshpsm  38979  islshpat  39016  cmtfvalN  39209  cmtvalN  39210  ishlat1  39351  ishlat2  39352  3dim0  39456  2dim  39469  islvol5  39578  lhpexle3  40011  cdleme0ex2N  40223  cdleme0nex  40289  cdlemg2cex  40590  cdlemg33b0  40700  cdlemg33b  40706  cdlemg33c  40707  cdlemg33e  40709  dib1dim  41164  diblsmopel  41170  dihopelvalcpre  41247  lcfls1c  41535  aks6d1c1p1  42100  aks6d1c1p1rcl  42101  sn-sup2  42484  sn-isghm  42666  3anrabdioph  42775  fgraphxp  43197  omge2  43291  faosnf0.11b  43420  dfsucon  43516  pren2  43546  dfrtrcl5  43622  brfvrcld2  43685  df3an2  43762  dfvd3  44585  3impexpVD  44849  modelaxreplem1  44972  rfcnnnub  45034  stoweidlem35  46036  smflimlem4  46775  ndmaovass  47210  nltle2tri  47317  elfz2z  47319  prproropf1olem0  47506  reuprpr  47527  gboge9  47768  sbgoldbalt  47785  nnsum4primesodd  47800  nnsum4primesoddALTV  47801  bgoldbtbndlem4  47812  bgoldbtbnd  47813  dfvopnbgr2  47857  isuspgrim  47900  isubgr3stgrlem7  47976  grlimprop2  47990  uhgrimgrlim  47991  pgn4cyclex  48130  rngcsectALTV  48279  rngcinvALTV  48280  ringcsectALTV  48313  ringcinvALTV  48314  islindeps  48458  islindeps2  48488  isldepslvec2  48490  elbigo2  48557  line2ylem  48756  io1ii  48925  catprsc  49018  0funcglem  49088  0funclem  49091  catcsect  49403  isthincd2  49442  thincsect  49472  2arwcatlem1  49600