Definition df-3an 1007

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 1005	. 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  1009  3anrot  1010  3ancoma  1012  3anan32  1016  3ioran  1020  3simpa  1021  3pm3.2i  1202  pm3.2an3  1203  3jca  1204  3anbi123i  1215  3imp  1220  3anbi123d  1349  3anim123d  1356  an6  1358  19.26-3an  1532  hb3an  1599  nf3an  1615  nf3and  1618  eeeanv  1989  sb3an  2014  mopick2  2166  r19.26-3  2675  3reeanv  2716  ceqsex3v  2859  ceqsex4v  2860  ceqsex8v  2862  sbc3an  3106  elin3  3412  rexdifpr  3719  raltpg  3744  tpss  3864  dfopg  3883  opeq1  3885  opeq2  3886  opm  4352  otth2  4359  poirr  4430  po3nr  4433  wepo  4482  wetrep  4483  rabxp  4789  brinxp2  4819  brinxp  4820  sotri2  5162  sotri3  5163  f1orn  5626  dff1o6  5951  isosolem  5999  oprabid  6084  caovimo  6250  elovmpo  6255  elovmporab  6256  elovmporab1w  6257  dfxp3  6392  nnaord  6744  fiintim  7193  prmuloc  7883  ltrelxr  8336  rexuz2  9916  ltxr  10111  elixx3g  10237  elioo4g  10270  elioopnf  10303  elioomnf  10304  elicopnf  10305  elxrge0  10314  divelunit  10338  elfz2  10352  elfzuzb  10356  uzsplit  10430  fznn0  10451  elfzmlbp  10470  elfzo2  10488  fzolb2  10493  fzouzsplit  10519  ssfzo12bi  10574  fzind2  10589  dfrp2  10627  ccatsymb  11294  swrdsbslen  11362  swrdspsleq  11363  swrdccatin2  11425  pfxccatin12lem2  11427  pfxccatin12lem3  11428  pfxccatin12  11429  pfxccat3a  11434  abs2dif  11795  sumeq2  12048  divalgb  12615  bitsval2  12634  divgcdz  12671  rplpwr  12727  nnwosdc  12739  cncongr1  12804  pythagtriplem2  12968  pythagtrip  12985  ballotfilemelo  13145  xpscf  13577  issgrpd  13642  issubm2  13703  issubg3  13926  resgrpisgrp  13929  eqgval  13957  eqger  13958  eqgabl  14064  qusecsub  14065  rnglz  14106  rngpropd  14116  ringpropd  14199  ringrghm  14223  zndvds  14814  znleval  14818  znleval2  14819  isbasis3g  14928  lmfval  15075  lmbr  15095  lmbr2  15096  xmeterval  15317  xmeter  15318  cnbl0  15416  cnblcld  15417  limcrcl  15540  gausslemma2dlem1a  15948  umgr2edg1  16221  subusgr  16287  upgriswlkdc  16372  clwwlknon2x  16447  bd3an  16617