Definition df-3an 983

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 981	. 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  985  3anrot  986  3ancoma  988  3anan32  992  3ioran  996  3simpa  997  3pm3.2i  1178  pm3.2an3  1179  3jca  1180  3anbi123i  1191  3imp  1196  3anbi123d  1325  3anim123d  1332  an6  1334  19.26-3an  1507  hb3an  1574  nf3an  1590  nf3and  1593  eeeanv  1962  sb3an  1987  mopick2  2139  r19.26-3  2638  3reeanv  2679  ceqsex3v  2820  ceqsex4v  2821  ceqsex8v  2823  sbc3an  3067  elin3  3372  rexdifpr  3671  raltpg  3696  tpss  3812  dfopg  3831  opeq1  3833  opeq2  3834  opm  4296  otth2  4303  poirr  4372  po3nr  4375  wepo  4424  wetrep  4425  rabxp  4730  brinxp2  4760  brinxp  4761  sotri2  5099  sotri3  5100  f1orn  5554  dff1o6  5868  isosolem  5916  oprabid  5999  caovimo  6163  elovmpo  6168  elovmporab  6169  elovmporab1w  6170  dfxp3  6303  nnaord  6618  fiintim  7054  prmuloc  7714  ltrelxr  8168  rexuz2  9737  ltxr  9932  elixx3g  10058  elioo4g  10091  elioopnf  10124  elioomnf  10125  elicopnf  10126  elxrge0  10135  divelunit  10159  elfz2  10172  elfzuzb  10176  uzsplit  10249  fznn0  10270  elfzmlbp  10289  elfzo2  10307  fzolb2  10312  fzouzsplit  10338  ssfzo12bi  10391  fzind2  10405  dfrp2  10443  ccatsymb  11096  swrdsbslen  11157  swrdspsleq  11158  swrdccatin2  11220  pfxccatin12lem2  11222  pfxccatin12lem3  11223  pfxccatin12  11224  pfxccat3a  11229  abs2dif  11532  sumeq2  11785  divalgb  12351  bitsval2  12370  divgcdz  12407  rplpwr  12463  nnwosdc  12475  cncongr1  12540  pythagtriplem2  12704  pythagtrip  12721  xpscf  13294  issgrpd  13359  issubm2  13420  issubg3  13643  resgrpisgrp  13646  eqgval  13674  eqger  13675  eqgabl  13781  qusecsub  13782  rnglz  13822  rngpropd  13832  ringpropd  13915  ringrghm  13939  zndvds  14526  znleval  14530  znleval2  14531  isbasis3g  14633  lmfval  14779  lmbr  14800  lmbr2  14801  xmeterval  15022  xmeter  15023  cnbl0  15121  cnblcld  15122  limcrcl  15245  gausslemma2dlem1a  15650  bd3an  15965