Definition df-3an 887

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 885	. 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  889  3anrot  890  3ancoma  892  3anan32  896  3ioran  900  3simpa  901  3pm3.2i  1082  pm3.2an3  1083  3jca  1084  3anbi123i  1093  3imp  1098  3anbi123d  1207  3anim123d  1214  an6  1216  19.26-3an  1372  hb3an  1442  nf3an  1458  nf3and  1461  eeeanv  1808  sb3an  1832  mopick2  1983  r19.26-3  2440  3reeanv  2477  ceqsex3v  2593  ceqsex4v  2594  ceqsex8v  2596  elin3  3125  raltpg  3420  tpss  3526  dfopg  3544  opeq1  3546  opeq2  3547  opm  3968  otth2  3975  poirr  4041  po3nr  4044  rabxp  4358  brinxp2  4385  brinxp  4386  sotri2  4700  sotri3  4701  f1orn  5114  dff1o6  5394  isosolem  5441  oprabid  5515  caovimo  5672  elovmpt2  5679  dfxp3  5798  nnaord  6060  prmuloc  6636  ltrelxr  7051  rexuz2  8487  ltxr  8653  elixx3g  8728  elioo4g  8761  elioopnf  8794  elioomnf  8795  elicopnf  8796  elxrge0  8805  divelunit  8828  elfz2  8839  elfzuzb  8842  uzsplit  8912  fznn0  8932  elfzmlbp  8948  elfzo2  8965  fzolb2  8968  fzouzsplit  8993  ssfzo12bi  9039  fzind2  9053  abs2dif  9571  bd3an  9814