Definition df-3an 1011

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 405. (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 1009	. 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 used by:  3anass  1013  3anrot  1014  3ancoma  1016  3anan32  1020  3ioran  1024  3simpa  1025  3pm3.2i  1206  pm3.2an3  1207  3jca  1208  3anbi123i  1219  3imp  1224  3anbi123d  1353  3anim123d  1360  an6  1362  19.26-3an  1536  hb3an  1603  nf3an  1619  nf3and  1622  eeeanv  1993  sb3an  2018  mopick2  2170  r19.26-3  2681  3reeanv  2722  ceqsex3v  2865  ceqsex4v  2866  ceqsex8v  2868  sbc3an  3113  elin3  3420  rexdifpr  3737  raltpg  3762  tpss  3883  dfopg  3902  opeq1  3904  opeq2  3905  opm  4376  otth2  4383  poirr  4454  po3nr  4457  wepo  4506  wetrep  4507  rabxp  4814  brinxp2  4844  brinxp  4845  sotri2  5188  sotri3  5189  f1orn  5652  dff1o6  5985  isosolem  6033  oprabid  6120  caovimo  6286  elovmpo  6291  elovmporab  6292  elovmporab1w  6293  dfxp3  6434  nnaord  6786  fiintim  7242  prmuloc  7939  ltrelxr  8392  rexuz2  9997  ltxr  10194  elixx3g  10320  elioo4g  10353  elioopnf  10386  elioomnf  10387  elicopnf  10388  elxrge0  10397  divelunit  10421  elfz2  10435  elfzuzb  10439  uzsplit  10516  fznn0  10537  elfzmlbp  10556  elfzo2  10574  fzolb2  10579  fzouzsplit  10605  ssfzo12bi  10660  fzind2  10675  dfrp2  10715  ccatsymb  11392  swrdsbslen  11460  swrdspsleq  11461  swrdccatin2  11523  pfxccatin12lem2  11525  pfxccatin12lem3  11526  pfxccatin12  11527  pfxccat3a  11532  abs2dif  11895  sumeq2  12150  divalgb  12717  bitsval2  12736  divgcdz  12773  rplpwr  12829  nnwosdc  12841  cncongr1  12906  pythagtriplem2  13074  pythagtrip  13091  ballotfilemelo  13280  xpscf  13727  issgrpd  13786  issubm2  13839  issubg3  14054  resgrpisgrp  14057  eqgval  14085  eqger  14086  eqgabl  14224  qusecsub  14225  rnglz  14351  rngpropd  14361  ringpropd  14450  ringrghm  14474  zndvds  15093  znleval  15097  znleval2  15098  isbasis3g  15272  lmfval  15419  lmbr  15439  lmbr2  15440  xmeterval  15661  xmeter  15662  cnbl0  15760  cnblcld  15761  limcrcl  15884  gausslemma2dlem1a  16382  umgr2edg1  16655  subusgr  16721  upgriswlkdc  16806  clwwlknon2x  16881  bd3an  17061