Definition df-3an 1006

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 1004	. 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  1008  3anrot  1009  3ancoma  1011  3anan32  1015  3ioran  1019  3simpa  1020  3pm3.2i  1201  pm3.2an3  1202  3jca  1203  3anbi123i  1214  3imp  1219  3anbi123d  1348  3anim123d  1355  an6  1357  19.26-3an  1531  hb3an  1598  nf3an  1614  nf3and  1617  eeeanv  1986  sb3an  2011  mopick2  2163  r19.26-3  2663  3reeanv  2704  ceqsex3v  2846  ceqsex4v  2847  ceqsex8v  2849  sbc3an  3093  elin3  3398  rexdifpr  3697  raltpg  3722  tpss  3841  dfopg  3860  opeq1  3862  opeq2  3863  opm  4326  otth2  4333  poirr  4404  po3nr  4407  wepo  4456  wetrep  4457  rabxp  4763  brinxp2  4793  brinxp  4794  sotri2  5134  sotri3  5135  f1orn  5593  dff1o6  5916  isosolem  5964  oprabid  6049  caovimo  6215  elovmpo  6220  elovmporab  6221  elovmporab1w  6222  dfxp3  6358  nnaord  6676  fiintim  7122  prmuloc  7785  ltrelxr  8239  rexuz2  9814  ltxr  10009  elixx3g  10135  elioo4g  10168  elioopnf  10201  elioomnf  10202  elicopnf  10203  elxrge0  10212  divelunit  10236  elfz2  10249  elfzuzb  10253  uzsplit  10326  fznn0  10347  elfzmlbp  10366  elfzo2  10384  fzolb2  10389  fzouzsplit  10415  ssfzo12bi  10469  fzind2  10484  dfrp2  10522  ccatsymb  11178  swrdsbslen  11246  swrdspsleq  11247  swrdccatin2  11309  pfxccatin12lem2  11311  pfxccatin12lem3  11312  pfxccatin12  11313  pfxccat3a  11318  abs2dif  11666  sumeq2  11919  divalgb  12485  bitsval2  12504  divgcdz  12541  rplpwr  12597  nnwosdc  12609  cncongr1  12674  pythagtriplem2  12838  pythagtrip  12855  xpscf  13429  issgrpd  13494  issubm2  13555  issubg3  13778  resgrpisgrp  13781  eqgval  13809  eqger  13810  eqgabl  13916  qusecsub  13917  rnglz  13957  rngpropd  13967  ringpropd  14050  ringrghm  14074  zndvds  14662  znleval  14666  znleval2  14667  isbasis3g  14769  lmfval  14916  lmbr  14936  lmbr2  14937  xmeterval  15158  xmeter  15159  cnbl0  15257  cnblcld  15258  limcrcl  15381  gausslemma2dlem1a  15786  umgr2edg1  16059  subusgr  16125  upgriswlkdc  16210  clwwlknon2x  16285  bd3an  16425