Definition df-3an 983

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 981	. 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  985  3anrot  986  3ancoma  988  3anan32  992  3ioran  996  3simpa  997  3pm3.2i  1178  pm3.2an3  1179  3jca  1180  3anbi123i  1191  3imp  1196  3anbi123d  1325  3anim123d  1332  an6  1334  19.26-3an  1507  hb3an  1574  nf3an  1590  nf3and  1593  eeeanv  1962  sb3an  1987  mopick2  2138  r19.26-3  2637  3reeanv  2678  ceqsex3v  2817  ceqsex4v  2818  ceqsex8v  2820  sbc3an  3062  elin3  3366  rexdifpr  3663  raltpg  3688  tpss  3802  dfopg  3820  opeq1  3822  opeq2  3823  opm  4283  otth2  4290  poirr  4359  po3nr  4362  wepo  4411  wetrep  4412  rabxp  4717  brinxp2  4747  brinxp  4748  sotri2  5086  sotri3  5087  f1orn  5541  dff1o6  5855  isosolem  5903  oprabid  5986  caovimo  6150  elovmpo  6155  elovmporab  6156  elovmporab1w  6157  dfxp3  6290  nnaord  6605  fiintim  7040  prmuloc  7692  ltrelxr  8146  rexuz2  9715  ltxr  9910  elixx3g  10036  elioo4g  10069  elioopnf  10102  elioomnf  10103  elicopnf  10104  elxrge0  10113  divelunit  10137  elfz2  10150  elfzuzb  10154  uzsplit  10227  fznn0  10248  elfzmlbp  10267  elfzo2  10285  fzolb2  10290  fzouzsplit  10316  ssfzo12bi  10367  fzind2  10381  dfrp2  10419  ccatsymb  11072  swrdsbslen  11133  swrdspsleq  11134  abs2dif  11467  sumeq2  11720  divalgb  12286  bitsval2  12305  divgcdz  12342  rplpwr  12398  nnwosdc  12410  cncongr1  12475  pythagtriplem2  12639  pythagtrip  12656  xpscf  13229  issgrpd  13294  issubm2  13355  issubg3  13578  resgrpisgrp  13581  eqgval  13609  eqger  13610  eqgabl  13716  qusecsub  13717  rnglz  13757  rngpropd  13767  ringpropd  13850  ringrghm  13874  zndvds  14461  znleval  14465  znleval2  14466  isbasis3g  14568  lmfval  14714  lmbr  14735  lmbr2  14736  xmeterval  14957  xmeter  14958  cnbl0  15056  cnblcld  15057  limcrcl  15180  gausslemma2dlem1a  15585  bd3an  15880