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  2843  ceqsex4v  2844  ceqsex8v  2846  sbc3an  3090  elin3  3395  rexdifpr  3694  raltpg  3719  tpss  3835  dfopg  3854  opeq1  3856  opeq2  3857  opm  4319  otth2  4326  poirr  4395  po3nr  4398  wepo  4447  wetrep  4448  rabxp  4753  brinxp2  4783  brinxp  4784  sotri2  5122  sotri3  5123  f1orn  5578  dff1o6  5893  isosolem  5941  oprabid  6026  caovimo  6190  elovmpo  6195  elovmporab  6196  elovmporab1w  6197  dfxp3  6330  nnaord  6645  fiintim  7081  prmuloc  7741  ltrelxr  8195  rexuz2  9764  ltxr  9959  elixx3g  10085  elioo4g  10118  elioopnf  10151  elioomnf  10152  elicopnf  10153  elxrge0  10162  divelunit  10186  elfz2  10199  elfzuzb  10203  uzsplit  10276  fznn0  10297  elfzmlbp  10316  elfzo2  10334  fzolb2  10339  fzouzsplit  10365  ssfzo12bi  10418  fzind2  10432  dfrp2  10470  ccatsymb  11123  swrdsbslen  11184  swrdspsleq  11185  swrdccatin2  11247  pfxccatin12lem2  11249  pfxccatin12lem3  11250  pfxccatin12  11251  pfxccat3a  11256  abs2dif  11603  sumeq2  11856  divalgb  12422  bitsval2  12441  divgcdz  12478  rplpwr  12534  nnwosdc  12546  cncongr1  12611  pythagtriplem2  12775  pythagtrip  12792  xpscf  13366  issgrpd  13431  issubm2  13492  issubg3  13715  resgrpisgrp  13718  eqgval  13746  eqger  13747  eqgabl  13853  qusecsub  13854  rnglz  13894  rngpropd  13904  ringpropd  13987  ringrghm  14011  zndvds  14598  znleval  14602  znleval2  14603  isbasis3g  14705  lmfval  14851  lmbr  14872  lmbr2  14873  xmeterval  15094  xmeter  15095  cnbl0  15193  cnblcld  15194  limcrcl  15317  gausslemma2dlem1a  15722  umgr2edg1  15992  bd3an  16123