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  6545  ltrelxr  6837  rexuz2  8260  ltxr  8425  elixx3g  8500  elioo4g  8533  elioopnf  8566  elioomnf  8567  elicopnf  8568  elxrge0  8577  divelunit  8600  elfz2  8611  elfzuzb  8614  uzsplit  8684  fznn0  8704  elfzmlbp  8720  elfzo2  8737  fzolb2  8740  fzouzsplit  8765  ssfzo12bi  8811  fzind2  8825  bd3an  9219