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  1494  hb3an  1561  nf3an  1577  nf3and  1580  eeeanv  1949  sb3an  1974  mopick2  2125  r19.26-3  2624  3reeanv  2665  ceqsex3v  2803  ceqsex4v  2804  ceqsex8v  2806  sbc3an  3048  elin3  3351  rexdifpr  3647  raltpg  3672  tpss  3785  dfopg  3803  opeq1  3805  opeq2  3806  opm  4264  otth2  4271  poirr  4339  po3nr  4342  wepo  4391  wetrep  4392  rabxp  4697  brinxp2  4727  brinxp  4728  sotri2  5064  sotri3  5065  f1orn  5511  dff1o6  5820  isosolem  5868  oprabid  5951  caovimo  6114  elovmpo  6119  elovmporab  6120  elovmporab1w  6121  dfxp3  6249  nnaord  6564  fiintim  6987  prmuloc  7628  ltrelxr  8082  rexuz2  9649  ltxr  9844  elixx3g  9970  elioo4g  10003  elioopnf  10036  elioomnf  10037  elicopnf  10038  elxrge0  10047  divelunit  10071  elfz2  10084  elfzuzb  10088  uzsplit  10161  fznn0  10182  elfzmlbp  10201  elfzo2  10219  fzolb2  10224  fzouzsplit  10249  ssfzo12bi  10295  fzind2  10309  dfrp2  10335  abs2dif  11253  sumeq2  11505  divalgb  12069  divgcdz  12111  rplpwr  12167  nnwosdc  12179  cncongr1  12244  pythagtriplem2  12407  pythagtrip  12424  xpscf  12933  issgrpd  12998  issubm2  13048  issubg3  13265  resgrpisgrp  13268  eqgval  13296  eqger  13297  eqgabl  13403  qusecsub  13404  rnglz  13444  rngpropd  13454  ringpropd  13537  ringrghm  13561  zndvds  14148  znleval  14152  znleval2  14153  isbasis3g  14225  lmfval  14371  lmbr  14392  lmbr2  14393  xmeterval  14614  xmeter  14615  cnbl0  14713  cnblcld  14714  limcrcl  14837  gausslemma2dlem1a  15215  bd3an  15392