Definition df-3an 1007

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 1005	. 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  1009  3anrot  1010  3ancoma  1012  3anan32  1016  3ioran  1020  3simpa  1021  3pm3.2i  1202  pm3.2an3  1203  3jca  1204  3anbi123i  1215  3imp  1220  3anbi123d  1349  3anim123d  1356  an6  1358  19.26-3an  1532  hb3an  1599  nf3an  1615  nf3and  1618  eeeanv  1986  sb3an  2011  mopick2  2163  r19.26-3  2664  3reeanv  2705  ceqsex3v  2847  ceqsex4v  2848  ceqsex8v  2850  sbc3an  3094  elin3  3400  rexdifpr  3701  raltpg  3726  tpss  3846  dfopg  3865  opeq1  3867  opeq2  3868  opm  4332  otth2  4339  poirr  4410  po3nr  4413  wepo  4462  wetrep  4463  rabxp  4769  brinxp2  4799  brinxp  4800  sotri2  5141  sotri3  5142  f1orn  5602  dff1o6  5927  isosolem  5975  oprabid  6060  caovimo  6226  elovmpo  6231  elovmporab  6232  elovmporab1w  6233  dfxp3  6368  nnaord  6720  fiintim  7166  prmuloc  7846  ltrelxr  8299  rexuz2  9876  ltxr  10071  elixx3g  10197  elioo4g  10230  elioopnf  10263  elioomnf  10264  elicopnf  10265  elxrge0  10274  divelunit  10298  elfz2  10312  elfzuzb  10316  uzsplit  10389  fznn0  10410  elfzmlbp  10429  elfzo2  10447  fzolb2  10452  fzouzsplit  10478  ssfzo12bi  10533  fzind2  10548  dfrp2  10586  ccatsymb  11245  swrdsbslen  11313  swrdspsleq  11314  swrdccatin2  11376  pfxccatin12lem2  11378  pfxccatin12lem3  11379  pfxccatin12  11380  pfxccat3a  11385  abs2dif  11746  sumeq2  11999  divalgb  12566  bitsval2  12585  divgcdz  12622  rplpwr  12678  nnwosdc  12690  cncongr1  12755  pythagtriplem2  12919  pythagtrip  12936  xpscf  13510  issgrpd  13575  issubm2  13636  issubg3  13859  resgrpisgrp  13862  eqgval  13890  eqger  13891  eqgabl  13997  qusecsub  13998  rnglz  14039  rngpropd  14049  ringpropd  14132  ringrghm  14156  zndvds  14745  znleval  14749  znleval2  14750  isbasis3g  14857  lmfval  15004  lmbr  15024  lmbr2  15025  xmeterval  15246  xmeter  15247  cnbl0  15345  cnblcld  15346  limcrcl  15469  gausslemma2dlem1a  15877  umgr2edg1  16150  subusgr  16216  upgriswlkdc  16301  clwwlknon2x  16376  bd3an  16546