Definition df-3an 1011

Description: Define conjunction ('and') of 3 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 405. (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 1009	. 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒)
5	1, 2	wa 104	. . 3 wff (𝜑 ∧ 𝜓)
6	5, 3	wa 104	. 2 wff ((𝜑 ∧ 𝜓) ∧ 𝜒)
7	4, 6	wb 105	1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))

This definition is used by:  3anass  1013  3anrot  1014  3ancoma  1016  3anan32  1020  3ioran  1024  3simpa  1025  3pm3.2i  1206  pm3.2an3  1207  3jca  1208  3anbi123i  1219  3imp  1224  3anbi123d  1353  3anim123d  1360  an6  1362  19.26-3an  1536  hb3an  1603  nf3an  1619  nf3and  1622  eeeanv  1993  sb3an  2018  mopick2  2170  r19.26-3  2681  3reeanv  2722  ceqsex3v  2865  ceqsex4v  2866  ceqsex8v  2868  sbc3an  3113  elin3  3420  rexdifpr  3737  raltpg  3762  tpss  3883  dfopg  3902  opeq1  3904  opeq2  3905  opm  4376  otth2  4383  poirr  4454  po3nr  4457  wepo  4506  wetrep  4507  rabxp  4814  brinxp2  4844  brinxp  4845  sotri2  5188  sotri3  5189  f1orn  5652  dff1o6  5985  isosolem  6033  oprabid  6120  caovimo  6286  elovmpo  6291  elovmporab  6292  elovmporab1w  6293  dfxp3  6434  nnaord  6787  fiintim  7244  prmuloc  7939  ltrelxr  8392  rexuz2  9996  ltxr  10193  elixx3g  10319  elioo4g  10352  elioopnf  10385  elioomnf  10386  elicopnf  10387  elxrge0  10396  divelunit  10420  elfz2  10434  elfzuzb  10438  uzsplit  10515  fznn0  10536  elfzmlbp  10555  elfzo2  10573  fzolb2  10578  fzouzsplit  10604  ssfzo12bi  10659  fzind2  10674  dfrp2  10714  ccatsymb  11391  swrdsbslen  11459  swrdspsleq  11460  swrdccatin2  11522  pfxccatin12lem2  11524  pfxccatin12lem3  11525  pfxccatin12  11526  pfxccat3a  11531  abs2dif  11894  sumeq2  12149  divalgb  12716  bitsval2  12735  divgcdz  12772  rplpwr  12828  nnwosdc  12840  cncongr1  12905  pythagtriplem2  13073  pythagtrip  13090  ballotfilemelo  13279  xpscf  13726  issgrpd  13785  issubm2  13838  issubg3  14053  resgrpisgrp  14056  eqgval  14084  eqger  14085  eqgabl  14223  qusecsub  14224  rnglz  14350  rngpropd  14360  ringpropd  14449  ringrghm  14473  zndvds  15092  znleval  15096  znleval2  15097  isbasis3g  15289  lmfval  15436  lmbr  15456  lmbr2  15457  xmeterval  15678  xmeter  15679  cnbl0  15777  cnblcld  15778  limcrcl  15901  gausslemma2dlem1a  16399  umgr2edg1  16672  subusgr  16738  upgriswlkdc  16823  clwwlknon2x  16898  bd3an  17078