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  5917  isosolem  5965  oprabid  6050  caovimo  6216  elovmpo  6221  elovmporab  6222  elovmporab1w  6223  dfxp3  6359  nnaord  6677  fiintim  7123  prmuloc  7786  ltrelxr  8240  rexuz2  9815  ltxr  10010  elixx3g  10136  elioo4g  10169  elioopnf  10202  elioomnf  10203  elicopnf  10204  elxrge0  10213  divelunit  10237  elfz2  10250  elfzuzb  10254  uzsplit  10327  fznn0  10348  elfzmlbp  10367  elfzo2  10385  fzolb2  10390  fzouzsplit  10416  ssfzo12bi  10471  fzind2  10486  dfrp2  10524  ccatsymb  11183  swrdsbslen  11251  swrdspsleq  11252  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatin12lem3  11317  pfxccatin12  11318  pfxccat3a  11323  abs2dif  11684  sumeq2  11937  divalgb  12504  bitsval2  12523  divgcdz  12560  rplpwr  12616  nnwosdc  12628  cncongr1  12693  pythagtriplem2  12857  pythagtrip  12874  xpscf  13448  issgrpd  13513  issubm2  13574  issubg3  13797  resgrpisgrp  13800  eqgval  13828  eqger  13829  eqgabl  13935  qusecsub  13936  rnglz  13977  rngpropd  13987  ringpropd  14070  ringrghm  14094  zndvds  14682  znleval  14686  znleval2  14687  isbasis3g  14789  lmfval  14936  lmbr  14956  lmbr2  14957  xmeterval  15178  xmeter  15179  cnbl0  15277  cnblcld  15278  limcrcl  15401  gausslemma2dlem1a  15806  umgr2edg1  16079  subusgr  16145  upgriswlkdc  16230  clwwlknon2x  16305  bd3an  16476