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  2647  ceqsex3v  2779  ceqsex4v  2780  ceqsex8v  2782  sbc3an  3024  elin3  3326  rexdifpr  3620  raltpg  3645  tpss  3758  dfopg  3776  opeq1  3778  opeq2  3779  opm  4234  otth2  4241  poirr  4307  po3nr  4310  wepo  4359  wetrep  4360  rabxp  4663  brinxp2  4693  brinxp  4694  sotri2  5026  sotri3  5027  f1orn  5471  dff1o6  5776  isosolem  5824  oprabid  5906  caovimo  6067  elovmpo  6071  dfxp3  6194  nnaord  6509  fiintim  6927  prmuloc  7564  ltrelxr  8017  rexuz2  9580  ltxr  9774  elixx3g  9900  elioo4g  9933  elioopnf  9966  elioomnf  9967  elicopnf  9968  elxrge0  9977  divelunit  10001  elfz2  10014  elfzuzb  10018  uzsplit  10091  fznn0  10112  elfzmlbp  10131  elfzo2  10149  fzolb2  10153  fzouzsplit  10178  ssfzo12bi  10224  fzind2  10238  dfrp2  10263  abs2dif  11114  sumeq2  11366  divalgb  11929  divgcdz  11971  rplpwr  12027  nnwosdc  12039  cncongr1  12102  pythagtriplem2  12265  pythagtrip  12282  xpscf  12765  issubm2  12863  issubg3  13050  resgrpisgrp  13053  eqgval  13080  eqger  13081  ringpropd  13215  isbasis3g  13516  lmfval  13662  lmbr  13683  lmbr2  13684  xmeterval  13905  xmeter  13906  cnbl0  14004  cnblcld  14005  limcrcl  14097  bd3an  14552