Definition df-3an 970

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 399. (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 968	. 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  972  3anrot  973  3ancoma  975  3anan32  979  3ioran  983  3simpa  984  3pm3.2i  1165  pm3.2an3  1166  3jca  1167  3anbi123i  1178  3imp  1183  3anbi123d  1302  3anim123d  1309  an6  1311  19.26-3an  1471  hb3an  1538  nf3an  1554  nf3and  1557  eeeanv  1921  sb3an  1946  mopick2  2097  r19.26-3  2595  3reeanv  2635  ceqsex3v  2767  ceqsex4v  2768  ceqsex8v  2770  sbc3an  3011  elin3  3312  rexdifpr  3603  raltpg  3628  tpss  3737  dfopg  3755  opeq1  3757  opeq2  3758  opm  4211  otth2  4218  poirr  4284  po3nr  4287  wepo  4336  wetrep  4337  rabxp  4640  brinxp2  4670  brinxp  4671  sotri2  5000  sotri3  5001  f1orn  5441  dff1o6  5743  isosolem  5791  oprabid  5870  caovimo  6031  elovmpo  6038  dfxp3  6159  nnaord  6473  fiintim  6890  prmuloc  7503  ltrelxr  7955  rexuz2  9515  ltxr  9707  elixx3g  9833  elioo4g  9866  elioopnf  9899  elioomnf  9900  elicopnf  9901  elxrge0  9910  divelunit  9934  elfz2  9947  elfzuzb  9950  uzsplit  10023  fznn0  10044  elfzmlbp  10063  elfzo2  10081  fzolb2  10085  fzouzsplit  10110  ssfzo12bi  10156  fzind2  10170  dfrp2  10195  abs2dif  11044  sumeq2  11296  divalgb  11858  divgcdz  11900  rplpwr  11956  nnwosdc  11968  cncongr1  12031  pythagtriplem2  12194  pythagtrip  12211  isbasis3g  12644  lmfval  12792  lmbr  12813  lmbr2  12814  xmeterval  13035  xmeter  13036  cnbl0  13134  cnblcld  13135  limcrcl  13227  bd3an  13672