Definition df-3an 1004

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 1002	. 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  1006  3anrot  1007  3ancoma  1009  3anan32  1013  3ioran  1017  3simpa  1018  3pm3.2i  1199  pm3.2an3  1200  3jca  1201  3anbi123i  1212  3imp  1217  3anbi123d  1346  3anim123d  1353  an6  1355  19.26-3an  1529  hb3an  1596  nf3an  1612  nf3and  1615  eeeanv  1984  sb3an  2009  mopick2  2161  r19.26-3  2661  3reeanv  2702  ceqsex3v  2844  ceqsex4v  2845  ceqsex8v  2847  sbc3an  3091  elin3  3396  rexdifpr  3695  raltpg  3720  tpss  3837  dfopg  3856  opeq1  3858  opeq2  3859  opm  4322  otth2  4329  poirr  4400  po3nr  4403  wepo  4452  wetrep  4453  rabxp  4759  brinxp2  4789  brinxp  4790  sotri2  5130  sotri3  5131  f1orn  5588  dff1o6  5910  isosolem  5958  oprabid  6043  caovimo  6209  elovmpo  6214  elovmporab  6215  elovmporab1w  6216  dfxp3  6352  nnaord  6670  fiintim  7114  prmuloc  7774  ltrelxr  8228  rexuz2  9803  ltxr  9998  elixx3g  10124  elioo4g  10157  elioopnf  10190  elioomnf  10191  elicopnf  10192  elxrge0  10201  divelunit  10225  elfz2  10238  elfzuzb  10242  uzsplit  10315  fznn0  10336  elfzmlbp  10355  elfzo2  10373  fzolb2  10378  fzouzsplit  10404  ssfzo12bi  10458  fzind2  10473  dfrp2  10511  ccatsymb  11166  swrdsbslen  11234  swrdspsleq  11235  swrdccatin2  11297  pfxccatin12lem2  11299  pfxccatin12lem3  11300  pfxccatin12  11301  pfxccat3a  11306  abs2dif  11654  sumeq2  11907  divalgb  12473  bitsval2  12492  divgcdz  12529  rplpwr  12585  nnwosdc  12597  cncongr1  12662  pythagtriplem2  12826  pythagtrip  12843  xpscf  13417  issgrpd  13482  issubm2  13543  issubg3  13766  resgrpisgrp  13769  eqgval  13797  eqger  13798  eqgabl  13904  qusecsub  13905  rnglz  13945  rngpropd  13955  ringpropd  14038  ringrghm  14062  zndvds  14650  znleval  14654  znleval2  14655  isbasis3g  14757  lmfval  14904  lmbr  14924  lmbr2  14925  xmeterval  15146  xmeter  15147  cnbl0  15245  cnblcld  15246  limcrcl  15369  gausslemma2dlem1a  15774  umgr2edg1  16044  upgriswlkdc  16148  clwwlknon2x  16220  bd3an  16335