Definition df-3an 886

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 381. (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 884	. 2 wff (φ ∧ ψ ∧ χ)
5	1, 2	wa 97	. . 3 wff (φ ∧ ψ)
6	5, 3	wa 97	. 2 wff ((φ ∧ ψ) ∧ χ)
7	4, 6	wb 98	1 wff ((φ ∧ ψ ∧ χ) ↔ ((φ ∧ ψ) ∧ χ))

This definition is referenced by:  3anass  888  3anrot  889  3ancoma  891  3anan32  895  3ioran  899  3simpa  900  3pm3.2i  1081  pm3.2an3  1082  3jca  1083  3anbi123i  1092  3imp  1097  3anbi123d  1206  3anim123d  1213  an6  1215  19.26-3an  1369  hb3an  1439  nf3an  1455  nf3and  1458  eeeanv  1805  sb3an  1829  mopick2  1980  r19.26-3  2437  3reeanv  2474  ceqsex3v  2590  ceqsex4v  2591  ceqsex8v  2593  elin3  3122  raltpg  3414  tpss  3520  dfopg  3538  opeq1  3540  opeq2  3541  opm  3962  otth2  3969  poirr  4035  po3nr  4038  rabxp  4323  brinxp2  4350  brinxp  4351  sotri2  4665  sotri3  4666  f1orn  5079  dff1o6  5359  isosolem  5406  oprabid  5480  caovimo  5636  elovmpt2  5643  dfxp3  5762  nnaord  6018  prmuloc  6547  ltrelxr  6877  rexuz2  8300  ltxr  8465  elixx3g  8540  elioo4g  8573  elioopnf  8606  elioomnf  8607  elicopnf  8608  elxrge0  8617  divelunit  8640  elfz2  8651  elfzuzb  8654  uzsplit  8724  fznn0  8744  elfzmlbp  8760  elfzo2  8777  fzolb2  8780  fzouzsplit  8805  ssfzo12bi  8851  fzind2  8865  bd3an  9285