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  2443  3reeanv  2480  ceqsex3v  2596  ceqsex4v  2597  ceqsex8v  2599  elin3  3128  raltpg  3423  tpss  3529  dfopg  3547  opeq1  3549  opeq2  3550  opm  3971  otth2  3978  poirr  4044  po3nr  4047  wepo  4096  wetrep  4097  rabxp  4380  brinxp2  4407  brinxp  4408  sotri2  4722  sotri3  4723  f1orn  5136  dff1o6  5416  isosolem  5463  oprabid  5537  caovimo  5694  elovmpt2  5701  dfxp3  5820  nnaord  6082  prmuloc  6664  ltrelxr  7080  rexuz2  8524  ltxr  8695  elixx3g  8770  elioo4g  8803  elioopnf  8836  elioomnf  8837  elicopnf  8838  elxrge0  8847  divelunit  8870  elfz2  8881  elfzuzb  8884  uzsplit  8954  fznn0  8974  elfzmlbp  8990  elfzo2  9007  fzolb2  9010  fzouzsplit  9035  ssfzo12bi  9081  fzind2  9095  abs2dif  9702  bd3an  9950