Definition df-3an 982

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 980	. 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  984  3anrot  985  3ancoma  987  3anan32  991  3ioran  995  3simpa  996  3pm3.2i  1177  pm3.2an3  1178  3jca  1179  3anbi123i  1190  3imp  1195  3anbi123d  1323  3anim123d  1330  an6  1332  19.26-3an  1497  hb3an  1564  nf3an  1580  nf3and  1583  eeeanv  1952  sb3an  1977  mopick2  2128  r19.26-3  2627  3reeanv  2668  ceqsex3v  2806  ceqsex4v  2807  ceqsex8v  2809  sbc3an  3051  elin3  3355  rexdifpr  3651  raltpg  3676  tpss  3789  dfopg  3807  opeq1  3809  opeq2  3810  opm  4268  otth2  4275  poirr  4343  po3nr  4346  wepo  4395  wetrep  4396  rabxp  4701  brinxp2  4731  brinxp  4732  sotri2  5068  sotri3  5069  f1orn  5517  dff1o6  5826  isosolem  5874  oprabid  5957  caovimo  6121  elovmpo  6126  elovmporab  6127  elovmporab1w  6128  dfxp3  6261  nnaord  6576  fiintim  7001  prmuloc  7652  ltrelxr  8106  rexuz2  9674  ltxr  9869  elixx3g  9995  elioo4g  10028  elioopnf  10061  elioomnf  10062  elicopnf  10063  elxrge0  10072  divelunit  10096  elfz2  10109  elfzuzb  10113  uzsplit  10186  fznn0  10207  elfzmlbp  10226  elfzo2  10244  fzolb2  10249  fzouzsplit  10274  ssfzo12bi  10320  fzind2  10334  dfrp2  10372  abs2dif  11290  sumeq2  11543  divalgb  12109  bitsval2  12128  divgcdz  12165  rplpwr  12221  nnwosdc  12233  cncongr1  12298  pythagtriplem2  12462  pythagtrip  12479  xpscf  13051  issgrpd  13116  issubm2  13177  issubg3  13400  resgrpisgrp  13403  eqgval  13431  eqger  13432  eqgabl  13538  qusecsub  13539  rnglz  13579  rngpropd  13589  ringpropd  13672  ringrghm  13696  zndvds  14283  znleval  14287  znleval2  14288  isbasis3g  14390  lmfval  14536  lmbr  14557  lmbr2  14558  xmeterval  14779  xmeter  14780  cnbl0  14878  cnblcld  14879  limcrcl  15002  gausslemma2dlem1a  15407  bd3an  15584