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  3836  dfopg  3855  opeq1  3857  opeq2  3858  opm  4320  otth2  4327  poirr  4398  po3nr  4401  wepo  4450  wetrep  4451  rabxp  4756  brinxp2  4786  brinxp  4787  sotri2  5126  sotri3  5127  f1orn  5584  dff1o6  5906  isosolem  5954  oprabid  6039  caovimo  6205  elovmpo  6210  elovmporab  6211  elovmporab1w  6212  dfxp3  6346  nnaord  6663  fiintim  7101  prmuloc  7761  ltrelxr  8215  rexuz2  9784  ltxr  9979  elixx3g  10105  elioo4g  10138  elioopnf  10171  elioomnf  10172  elicopnf  10173  elxrge0  10182  divelunit  10206  elfz2  10219  elfzuzb  10223  uzsplit  10296  fznn0  10317  elfzmlbp  10336  elfzo2  10354  fzolb2  10359  fzouzsplit  10385  ssfzo12bi  10439  fzind2  10453  dfrp2  10491  ccatsymb  11145  swrdsbslen  11206  swrdspsleq  11207  swrdccatin2  11269  pfxccatin12lem2  11271  pfxccatin12lem3  11272  pfxccatin12  11273  pfxccat3a  11278  abs2dif  11625  sumeq2  11878  divalgb  12444  bitsval2  12463  divgcdz  12500  rplpwr  12556  nnwosdc  12568  cncongr1  12633  pythagtriplem2  12797  pythagtrip  12814  xpscf  13388  issgrpd  13453  issubm2  13514  issubg3  13737  resgrpisgrp  13740  eqgval  13768  eqger  13769  eqgabl  13875  qusecsub  13876  rnglz  13916  rngpropd  13926  ringpropd  14009  ringrghm  14033  zndvds  14621  znleval  14625  znleval2  14626  isbasis3g  14728  lmfval  14875  lmbr  14895  lmbr2  14896  xmeterval  15117  xmeter  15118  cnbl0  15216  cnblcld  15217  limcrcl  15340  gausslemma2dlem1a  15745  umgr2edg1  16015  upgriswlkdc  16081  bd3an  16217