Definition df-3an 980

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

This definition is referenced by:  3anass  982  3anrot  983  3ancoma  985  3anan32  989  3ioran  993  3simpa  994  3pm3.2i  1175  pm3.2an3  1176  3jca  1177  3anbi123i  1188  3imp  1193  3anbi123d  1312  3anim123d  1319  an6  1321  19.26-3an  1483  hb3an  1550  nf3an  1566  nf3and  1569  eeeanv  1933  sb3an  1958  mopick2  2109  r19.26-3  2607  3reeanv  2647  ceqsex3v  2779  ceqsex4v  2780  ceqsex8v  2782  sbc3an  3024  elin3  3326  rexdifpr  3620  raltpg  3645  tpss  3757  dfopg  3775  opeq1  3777  opeq2  3778  opm  4232  otth2  4239  poirr  4305  po3nr  4308  wepo  4357  wetrep  4358  rabxp  4661  brinxp2  4691  brinxp  4692  sotri2  5023  sotri3  5024  f1orn  5468  dff1o6  5772  isosolem  5820  oprabid  5902  caovimo  6063  elovmpo  6067  dfxp3  6190  nnaord  6505  fiintim  6923  prmuloc  7560  ltrelxr  8012  rexuz2  9575  ltxr  9769  elixx3g  9895  elioo4g  9928  elioopnf  9961  elioomnf  9962  elicopnf  9963  elxrge0  9972  divelunit  9996  elfz2  10009  elfzuzb  10012  uzsplit  10085  fznn0  10106  elfzmlbp  10125  elfzo2  10143  fzolb2  10147  fzouzsplit  10172  ssfzo12bi  10218  fzind2  10232  dfrp2  10257  abs2dif  11106  sumeq2  11358  divalgb  11920  divgcdz  11962  rplpwr  12018  nnwosdc  12030  cncongr1  12093  pythagtriplem2  12256  pythagtrip  12273  issubm2  12792  issubg3  12978  resgrpisgrp  12981  ringpropd  13117  isbasis3g  13326  lmfval  13474  lmbr  13495  lmbr2  13496  xmeterval  13717  xmeter  13718  cnbl0  13816  cnblcld  13817  limcrcl  13909  bd3an  14353