Definition df-3an 964

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 398. (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 962	. 2 wff (𝜑 ∧ 𝜓 ∧ 𝜒)
5	1, 2	wa 103	. . 3 wff (𝜑 ∧ 𝜓)
6	5, 3	wa 103	. 2 wff ((𝜑 ∧ 𝜓) ∧ 𝜒)
7	4, 6	wb 104	1 wff ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))

This definition is referenced by:  3anass  966  3anrot  967  3ancoma  969  3anan32  973  3ioran  977  3simpa  978  3pm3.2i  1159  pm3.2an3  1160  3jca  1161  3anbi123i  1170  3imp  1175  3anbi123d  1290  3anim123d  1297  an6  1299  19.26-3an  1459  hb3an  1529  nf3an  1545  nf3and  1548  eeeanv  1905  sb3an  1931  mopick2  2082  r19.26-3  2562  3reeanv  2601  ceqsex3v  2728  ceqsex4v  2729  ceqsex8v  2731  sbc3an  2970  elin3  3267  raltpg  3576  tpss  3685  dfopg  3703  opeq1  3705  opeq2  3706  opm  4156  otth2  4163  poirr  4229  po3nr  4232  wepo  4281  wetrep  4282  rabxp  4576  brinxp2  4606  brinxp  4607  sotri2  4936  sotri3  4937  f1orn  5377  dff1o6  5677  isosolem  5725  oprabid  5803  caovimo  5964  elovmpo  5971  dfxp3  6092  nnaord  6405  fiintim  6817  prmuloc  7374  ltrelxr  7825  rexuz2  9376  ltxr  9562  elixx3g  9684  elioo4g  9717  elioopnf  9750  elioomnf  9751  elicopnf  9752  elxrge0  9761  divelunit  9785  elfz2  9797  elfzuzb  9800  uzsplit  9872  fznn0  9893  elfzmlbp  9909  elfzo2  9927  fzolb2  9931  fzouzsplit  9956  ssfzo12bi  10002  fzind2  10016  abs2dif  10878  sumeq2  11128  divalgb  11622  divgcdz  11660  rplpwr  11715  cncongr1  11784  isbasis3g  12213  lmfval  12361  lmbr  12382  lmbr2  12383  xmeterval  12604  xmeter  12605  cnbl0  12703  cnblcld  12704  limcrcl  12796  bd3an  13028