Definition df-3an 982

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	|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )

Detailed syntax breakdown of Definition df-3an

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3		wch	. . 3 wff ch
4	1, 2, 3	w3a 980	. 2 wff ( ph /\ ps /\ ch )
5	1, 2	wa 104	. . 3 wff ( ph /\ ps )
6	5, 3	wa 104	. 2 wff ( ( ph /\ ps ) /\ ch )
7	4, 6	wb 105	1 wff ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )

This definition is referenced by:  3anass  984  3anrot  985  3ancoma  987  3anan32  991  3ioran  995  3simpa  996  3pm3.2i  1177  pm3.2an3  1178  3jca  1179  3anbi123i  1190  3imp  1195  3anbi123d  1323  3anim123d  1330  an6  1332  19.26-3an  1497  hb3an  1564  nf3an  1580  nf3and  1583  eeeanv  1952  sb3an  1977  mopick2  2128  r19.26-3  2627  3reeanv  2668  ceqsex3v  2806  ceqsex4v  2807  ceqsex8v  2809  sbc3an  3051  elin3  3354  rexdifpr  3650  raltpg  3675  tpss  3788  dfopg  3806  opeq1  3808  opeq2  3809  opm  4267  otth2  4274  poirr  4342  po3nr  4345  wepo  4394  wetrep  4395  rabxp  4700  brinxp2  4730  brinxp  4731  sotri2  5067  sotri3  5068  f1orn  5514  dff1o6  5823  isosolem  5871  oprabid  5954  caovimo  6117  elovmpo  6122  elovmporab  6123  elovmporab1w  6124  dfxp3  6252  nnaord  6567  fiintim  6992  prmuloc  7633  ltrelxr  8087  rexuz2  9655  ltxr  9850  elixx3g  9976  elioo4g  10009  elioopnf  10042  elioomnf  10043  elicopnf  10044  elxrge0  10053  divelunit  10077  elfz2  10090  elfzuzb  10094  uzsplit  10167  fznn0  10188  elfzmlbp  10207  elfzo2  10225  fzolb2  10230  fzouzsplit  10255  ssfzo12bi  10301  fzind2  10315  dfrp2  10353  abs2dif  11271  sumeq2  11524  divalgb  12090  bitsval2  12109  divgcdz  12138  rplpwr  12194  nnwosdc  12206  cncongr1  12271  pythagtriplem2  12435  pythagtrip  12452  xpscf  12990  issgrpd  13055  issubm2  13105  issubg3  13322  resgrpisgrp  13325  eqgval  13353  eqger  13354  eqgabl  13460  qusecsub  13461  rnglz  13501  rngpropd  13511  ringpropd  13594  ringrghm  13618  zndvds  14205  znleval  14209  znleval2  14210  isbasis3g  14282  lmfval  14428  lmbr  14449  lmbr2  14450  xmeterval  14671  xmeter  14672  cnbl0  14770  cnblcld  14771  limcrcl  14894  gausslemma2dlem1a  15299  bd3an  15476