Definition df-3an 970

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 399. (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 968	. 2 wff ( ph /\ ps /\ ch )
5	1, 2	wa 103	. . 3 wff ( ph /\ ps )
6	5, 3	wa 103	. 2 wff ( ( ph /\ ps ) /\ ch )
7	4, 6	wb 104	1 wff ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )

This definition is referenced by:  3anass  972  3anrot  973  3ancoma  975  3anan32  979  3ioran  983  3simpa  984  3pm3.2i  1165  pm3.2an3  1166  3jca  1167  3anbi123i  1178  3imp  1183  3anbi123d  1302  3anim123d  1309  an6  1311  19.26-3an  1471  hb3an  1538  nf3an  1554  nf3and  1557  eeeanv  1921  sb3an  1946  mopick2  2097  r19.26-3  2596  3reeanv  2636  ceqsex3v  2768  ceqsex4v  2769  ceqsex8v  2771  sbc3an  3012  elin3  3313  rexdifpr  3604  raltpg  3629  tpss  3738  dfopg  3756  opeq1  3758  opeq2  3759  opm  4212  otth2  4219  poirr  4285  po3nr  4288  wepo  4337  wetrep  4338  rabxp  4641  brinxp2  4671  brinxp  4672  sotri2  5001  sotri3  5002  f1orn  5442  dff1o6  5744  isosolem  5792  oprabid  5874  caovimo  6035  elovmpo  6039  dfxp3  6162  nnaord  6477  fiintim  6894  prmuloc  7507  ltrelxr  7959  rexuz2  9519  ltxr  9711  elixx3g  9837  elioo4g  9870  elioopnf  9903  elioomnf  9904  elicopnf  9905  elxrge0  9914  divelunit  9938  elfz2  9951  elfzuzb  9954  uzsplit  10027  fznn0  10048  elfzmlbp  10067  elfzo2  10085  fzolb2  10089  fzouzsplit  10114  ssfzo12bi  10160  fzind2  10174  dfrp2  10199  abs2dif  11048  sumeq2  11300  divalgb  11862  divgcdz  11904  rplpwr  11960  nnwosdc  11972  cncongr1  12035  pythagtriplem2  12198  pythagtrip  12215  isbasis3g  12684  lmfval  12832  lmbr  12853  lmbr2  12854  xmeterval  13075  xmeter  13076  cnbl0  13174  cnblcld  13175  limcrcl  13267  bd3an  13712