Definition df-3an 1006

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 1004	. 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  1008  3anrot  1009  3ancoma  1011  3anan32  1015  3ioran  1019  3simpa  1020  3pm3.2i  1201  pm3.2an3  1202  3jca  1203  3anbi123i  1214  3imp  1219  3anbi123d  1348  3anim123d  1355  an6  1357  19.26-3an  1531  hb3an  1598  nf3an  1614  nf3and  1617  eeeanv  1986  sb3an  2011  mopick2  2163  r19.26-3  2663  3reeanv  2704  ceqsex3v  2846  ceqsex4v  2847  ceqsex8v  2849  sbc3an  3093  elin3  3398  rexdifpr  3697  raltpg  3722  tpss  3841  dfopg  3860  opeq1  3862  opeq2  3863  opm  4326  otth2  4333  poirr  4404  po3nr  4407  wepo  4456  wetrep  4457  rabxp  4763  brinxp2  4793  brinxp  4794  sotri2  5134  sotri3  5135  f1orn  5594  dff1o6  5920  isosolem  5968  oprabid  6053  caovimo  6219  elovmpo  6224  elovmporab  6225  elovmporab1w  6226  dfxp3  6362  nnaord  6680  fiintim  7126  prmuloc  7789  ltrelxr  8243  rexuz2  9818  ltxr  10013  elixx3g  10139  elioo4g  10172  elioopnf  10205  elioomnf  10206  elicopnf  10207  elxrge0  10216  divelunit  10240  elfz2  10253  elfzuzb  10257  uzsplit  10330  fznn0  10351  elfzmlbp  10370  elfzo2  10388  fzolb2  10393  fzouzsplit  10419  ssfzo12bi  10474  fzind2  10489  dfrp2  10527  ccatsymb  11186  swrdsbslen  11254  swrdspsleq  11255  swrdccatin2  11317  pfxccatin12lem2  11319  pfxccatin12lem3  11320  pfxccatin12  11321  pfxccat3a  11326  abs2dif  11687  sumeq2  11940  divalgb  12507  bitsval2  12526  divgcdz  12563  rplpwr  12619  nnwosdc  12631  cncongr1  12696  pythagtriplem2  12860  pythagtrip  12877  xpscf  13451  issgrpd  13516  issubm2  13577  issubg3  13800  resgrpisgrp  13803  eqgval  13831  eqger  13832  eqgabl  13938  qusecsub  13939  rnglz  13980  rngpropd  13990  ringpropd  14073  ringrghm  14097  zndvds  14685  znleval  14689  znleval2  14690  isbasis3g  14797  lmfval  14944  lmbr  14964  lmbr2  14965  xmeterval  15186  xmeter  15187  cnbl0  15285  cnblcld  15286  limcrcl  15409  gausslemma2dlem1a  15814  umgr2edg1  16087  subusgr  16153  upgriswlkdc  16238  clwwlknon2x  16313  bd3an  16484