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 used 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  3737  raltpg  3762  tpss  3883  dfopg  3902  opeq1  3904  opeq2  3905  opm  4374  otth2  4381  poirr  4452  po3nr  4455  wepo  4504  wetrep  4505  rabxp  4812  brinxp2  4842  brinxp  4843  sotri2  5185  sotri3  5186  f1orn  5649  dff1o6  5982  isosolem  6030  oprabid  6117  caovimo  6283  elovmpo  6288  elovmporab  6289  elovmporab1w  6290  dfxp3  6430  nnaord  6782  fiintim  7238  prmuloc  7934  ltrelxr  8387  rexuz2  9991  ltxr  10188  elixx3g  10314  elioo4g  10347  elioopnf  10380  elioomnf  10381  elicopnf  10382  elxrge0  10391  divelunit  10415  elfz2  10429  elfzuzb  10433  uzsplit  10510  fznn0  10531  elfzmlbp  10550  elfzo2  10568  fzolb2  10573  fzouzsplit  10599  ssfzo12bi  10654  fzind2  10669  dfrp2  10709  ccatsymb  11386  swrdsbslen  11454  swrdspsleq  11455  swrdccatin2  11517  pfxccatin12lem2  11519  pfxccatin12lem3  11520  pfxccatin12  11521  pfxccat3a  11526  abs2dif  11889  sumeq2  12144  divalgb  12711  bitsval2  12730  divgcdz  12767  rplpwr  12823  nnwosdc  12835  cncongr1  12900  pythagtriplem2  13068  pythagtrip  13085  ballotfilemelo  13274  xpscf  13721  issgrpd  13780  issubm2  13833  issubg3  14048  resgrpisgrp  14051  eqgval  14079  eqger  14080  eqgabl  14218  qusecsub  14219  rnglz  14328  rngpropd  14338  ringpropd  14427  ringrghm  14451  zndvds  15068  znleval  15072  znleval2  15073  isbasis3g  15238  lmfval  15385  lmbr  15405  lmbr2  15406  xmeterval  15627  xmeter  15628  cnbl0  15726  cnblcld  15727  limcrcl  15850  gausslemma2dlem1a  16343  umgr2edg1  16616  subusgr  16682  upgriswlkdc  16767  clwwlknon2x  16842  bd3an  17022