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  1506  hb3an  1573  nf3an  1589  nf3and  1592  eeeanv  1961  sb3an  1986  mopick2  2137  r19.26-3  2636  3reeanv  2677  ceqsex3v  2815  ceqsex4v  2816  ceqsex8v  2818  sbc3an  3060  elin3  3364  rexdifpr  3661  raltpg  3686  tpss  3799  dfopg  3817  opeq1  3819  opeq2  3820  opm  4278  otth2  4285  poirr  4354  po3nr  4357  wepo  4406  wetrep  4407  rabxp  4712  brinxp2  4742  brinxp  4743  sotri2  5080  sotri3  5081  f1orn  5532  dff1o6  5845  isosolem  5893  oprabid  5976  caovimo  6140  elovmpo  6145  elovmporab  6146  elovmporab1w  6147  dfxp3  6280  nnaord  6595  fiintim  7028  prmuloc  7679  ltrelxr  8133  rexuz2  9702  ltxr  9897  elixx3g  10023  elioo4g  10056  elioopnf  10089  elioomnf  10090  elicopnf  10091  elxrge0  10100  divelunit  10124  elfz2  10137  elfzuzb  10141  uzsplit  10214  fznn0  10235  elfzmlbp  10254  elfzo2  10272  fzolb2  10277  fzouzsplit  10303  ssfzo12bi  10354  fzind2  10368  dfrp2  10406  ccatsymb  11058  swrdsbslen  11119  swrdspsleq  11120  abs2dif  11417  sumeq2  11670  divalgb  12236  bitsval2  12255  divgcdz  12292  rplpwr  12348  nnwosdc  12360  cncongr1  12425  pythagtriplem2  12589  pythagtrip  12606  xpscf  13179  issgrpd  13244  issubm2  13305  issubg3  13528  resgrpisgrp  13531  eqgval  13559  eqger  13560  eqgabl  13666  qusecsub  13667  rnglz  13707  rngpropd  13717  ringpropd  13800  ringrghm  13824  zndvds  14411  znleval  14415  znleval2  14416  isbasis3g  14518  lmfval  14664  lmbr  14685  lmbr2  14686  xmeterval  14907  xmeter  14908  cnbl0  15006  cnblcld  15007  limcrcl  15130  gausslemma2dlem1a  15535  bd3an  15766