Definition df-3an 1011

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 405. (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 1009	. 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  1013  3anrot  1014  3ancoma  1016  3anan32  1020  3ioran  1024  3simpa  1025  3pm3.2i  1206  pm3.2an3  1207  3jca  1208  3anbi123i  1219  3imp  1224  3anbi123d  1353  3anim123d  1360  an6  1362  19.26-3an  1536  hb3an  1603  nf3an  1619  nf3and  1622  eeeanv  1993  sb3an  2018  mopick2  2170  r19.26-3  2681  3reeanv  2722  ceqsex3v  2865  ceqsex4v  2866  ceqsex8v  2868  sbc3an  3113  elin3  3420  rexdifpr  3736  raltpg  3761  tpss  3881  dfopg  3900  opeq1  3902  opeq2  3903  opm  4372  otth2  4379  poirr  4450  po3nr  4453  wepo  4502  wetrep  4503  rabxp  4810  brinxp2  4840  brinxp  4841  sotri2  5183  sotri3  5184  f1orn  5647  dff1o6  5975  isosolem  6023  oprabid  6110  caovimo  6276  elovmpo  6281  elovmporab  6282  elovmporab1w  6283  dfxp3  6423  nnaord  6775  fiintim  7231  prmuloc  7926  ltrelxr  8379  rexuz2  9963  ltxr  10159  elixx3g  10285  elioo4g  10318  elioopnf  10351  elioomnf  10352  elicopnf  10353  elxrge0  10362  divelunit  10386  elfz2  10400  elfzuzb  10404  uzsplit  10480  fznn0  10501  elfzmlbp  10520  elfzo2  10538  fzolb2  10543  fzouzsplit  10569  ssfzo12bi  10624  fzind2  10639  dfrp2  10679  ccatsymb  11351  swrdsbslen  11419  swrdspsleq  11420  swrdccatin2  11482  pfxccatin12lem2  11484  pfxccatin12lem3  11485  pfxccatin12  11486  pfxccat3a  11491  abs2dif  11853  sumeq2  12106  divalgb  12673  bitsval2  12692  divgcdz  12729  rplpwr  12785  nnwosdc  12797  cncongr1  12862  pythagtriplem2  13026  pythagtrip  13043  ballotfilemelo  13203  xpscf  13648  issgrpd  13707  issubm2  13760  issubg3  13975  resgrpisgrp  13978  eqgval  14006  eqger  14007  eqgabl  14114  qusecsub  14115  rnglz  14222  rngpropd  14232  ringpropd  14319  ringrghm  14343  zndvds  14959  znleval  14963  znleval2  14964  isbasis3g  15073  lmfval  15220  lmbr  15240  lmbr2  15241  xmeterval  15462  xmeter  15463  cnbl0  15561  cnblcld  15562  limcrcl  15685  gausslemma2dlem1a  16094  umgr2edg1  16367  subusgr  16433  upgriswlkdc  16518  clwwlknon2x  16593  bd3an  16773