Definition df-3an 922

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 393. (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 920	. 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒)
5	1, 2	wa 102	. . 3 wff (𝜑 ∧ 𝜓)
6	5, 3	wa 102	. 2 wff ((𝜑 ∧ 𝜓) ∧ 𝜒)
7	4, 6	wb 103	1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))

This definition is referenced by:  3anass  924  3anrot  925  3ancoma  927  3anan32  931  3ioran  935  3simpa  936  3pm3.2i  1117  pm3.2an3  1118  3jca  1119  3anbi123i  1128  3imp  1133  3anbi123d  1244  3anim123d  1251  an6  1253  19.26-3an  1413  hb3an  1483  nf3an  1499  nf3and  1502  eeeanv  1850  sb3an  1874  mopick2  2025  r19.26-3  2488  3reeanv  2525  ceqsex3v  2642  ceqsex4v  2643  ceqsex8v  2645  sbc3an  2876  elin3  3164  raltpg  3453  tpss  3558  dfopg  3576  opeq1  3578  opeq2  3579  opm  3997  otth2  4004  poirr  4070  po3nr  4073  wepo  4122  wetrep  4123  rabxp  4406  brinxp2  4433  brinxp  4434  sotri2  4752  sotri3  4753  f1orn  5167  dff1o6  5447  isosolem  5494  oprabid  5568  caovimo  5725  elovmpt2  5732  dfxp3  5851  nnaord  6148  prmuloc  6818  ltrelxr  7240  rexuz2  8750  ltxr  8927  elixx3g  9000  elioo4g  9033  elioopnf  9066  elioomnf  9067  elicopnf  9068  elxrge0  9077  divelunit  9100  elfz2  9112  elfzuzb  9115  uzsplit  9185  fznn0  9206  elfzmlbp  9220  elfzo2  9237  fzolb2  9240  fzouzsplit  9265  ssfzo12bi  9311  fzind2  9325  abs2dif  10130  sumeq2d  10334  sumeq2  10335  divalgb  10469  divgcdz  10507  rplpwr  10560  cncongr1  10629  bd3an  10779