Definition df-3an 921

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 919	. 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  923  3anrot  924  3ancoma  926  3anan32  930  3ioran  934  3simpa  935  3pm3.2i  1116  pm3.2an3  1117  3jca  1118  3anbi123i  1127  3imp  1132  3anbi123d  1243  3anim123d  1250  an6  1252  19.26-3an  1412  hb3an  1482  nf3an  1498  nf3and  1501  eeeanv  1849  sb3an  1873  mopick2  2024  r19.26-3  2487  3reeanv  2524  ceqsex3v  2641  ceqsex4v  2642  ceqsex8v  2644  sbc3an  2875  elin3  3157  raltpg  3445  tpss  3550  dfopg  3568  opeq1  3570  opeq2  3571  opm  3989  otth2  3996  poirr  4062  po3nr  4065  wepo  4114  wetrep  4115  rabxp  4398  brinxp2  4425  brinxp  4426  sotri2  4742  sotri3  4743  f1orn  5156  dff1o6  5436  isosolem  5483  oprabid  5557  caovimo  5714  elovmpt2  5721  dfxp3  5840  nnaord  6105  prmuloc  6756  ltrelxr  7173  rexuz2  8669  ltxr  8849  elixx3g  8924  elioo4g  8957  elioopnf  8990  elioomnf  8991  elicopnf  8992  elxrge0  9001  divelunit  9024  elfz2  9036  elfzuzb  9039  uzsplit  9109  fznn0  9129  elfzmlbp  9143  elfzo2  9160  fzolb2  9163  fzouzsplit  9188  ssfzo12bi  9234  fzind2  9248  abs2dif  9992  divalgb  10325  divgcdz  10363  rplpwr  10416  cncongr1  10485  bd3an  10621