Definition df-3an 980

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 978	. 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  982  3anrot  983  3ancoma  985  3anan32  989  3ioran  993  3simpa  994  3pm3.2i  1175  pm3.2an3  1176  3jca  1177  3anbi123i  1188  3imp  1193  3anbi123d  1312  3anim123d  1319  an6  1321  19.26-3an  1483  hb3an  1550  nf3an  1566  nf3and  1569  eeeanv  1933  sb3an  1958  mopick2  2109  r19.26-3  2607  3reeanv  2648  ceqsex3v  2780  ceqsex4v  2781  ceqsex8v  2783  sbc3an  3025  elin3  3327  rexdifpr  3621  raltpg  3646  tpss  3759  dfopg  3777  opeq1  3779  opeq2  3780  opm  4235  otth2  4242  poirr  4308  po3nr  4311  wepo  4360  wetrep  4361  rabxp  4664  brinxp2  4694  brinxp  4695  sotri2  5027  sotri3  5028  f1orn  5472  dff1o6  5777  isosolem  5825  oprabid  5907  caovimo  6068  elovmpo  6072  dfxp3  6195  nnaord  6510  fiintim  6928  prmuloc  7565  ltrelxr  8018  rexuz2  9581  ltxr  9775  elixx3g  9901  elioo4g  9934  elioopnf  9967  elioomnf  9968  elicopnf  9969  elxrge0  9978  divelunit  10002  elfz2  10015  elfzuzb  10019  uzsplit  10092  fznn0  10113  elfzmlbp  10132  elfzo2  10150  fzolb2  10154  fzouzsplit  10179  ssfzo12bi  10225  fzind2  10239  dfrp2  10264  abs2dif  11115  sumeq2  11367  divalgb  11930  divgcdz  11972  rplpwr  12028  nnwosdc  12040  cncongr1  12103  pythagtriplem2  12266  pythagtrip  12283  xpscf  12766  issubm2  12864  issubg3  13052  resgrpisgrp  13055  eqgval  13082  eqger  13083  ringpropd  13217  isbasis3g  13549  lmfval  13695  lmbr  13716  lmbr2  13717  xmeterval  13938  xmeter  13939  cnbl0  14037  cnblcld  14038  limcrcl  14130  bd3an  14585