Definition df-3an 982

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 980	. 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  984  3anrot  985  3ancoma  987  3anan32  991  3ioran  995  3simpa  996  3pm3.2i  1177  pm3.2an3  1178  3jca  1179  3anbi123i  1190  3imp  1195  3anbi123d  1324  3anim123d  1331  an6  1333  19.26-3an  1505  hb3an  1572  nf3an  1588  nf3and  1591  eeeanv  1960  sb3an  1985  mopick2  2136  r19.26-3  2635  3reeanv  2676  ceqsex3v  2814  ceqsex4v  2815  ceqsex8v  2817  sbc3an  3059  elin3  3363  rexdifpr  3660  raltpg  3685  tpss  3798  dfopg  3816  opeq1  3818  opeq2  3819  opm  4277  otth2  4284  poirr  4353  po3nr  4356  wepo  4405  wetrep  4406  rabxp  4711  brinxp2  4741  brinxp  4742  sotri2  5079  sotri3  5080  f1orn  5531  dff1o6  5844  isosolem  5892  oprabid  5975  caovimo  6139  elovmpo  6144  elovmporab  6145  elovmporab1w  6146  dfxp3  6279  nnaord  6594  fiintim  7027  prmuloc  7678  ltrelxr  8132  rexuz2  9701  ltxr  9896  elixx3g  10022  elioo4g  10055  elioopnf  10088  elioomnf  10089  elicopnf  10090  elxrge0  10099  divelunit  10123  elfz2  10136  elfzuzb  10140  uzsplit  10213  fznn0  10234  elfzmlbp  10253  elfzo2  10271  fzolb2  10276  fzouzsplit  10301  ssfzo12bi  10352  fzind2  10366  dfrp2  10404  ccatsymb  11056  abs2dif  11388  sumeq2  11641  divalgb  12207  bitsval2  12226  divgcdz  12263  rplpwr  12319  nnwosdc  12331  cncongr1  12396  pythagtriplem2  12560  pythagtrip  12577  xpscf  13150  issgrpd  13215  issubm2  13276  issubg3  13499  resgrpisgrp  13502  eqgval  13530  eqger  13531  eqgabl  13637  qusecsub  13638  rnglz  13678  rngpropd  13688  ringpropd  13771  ringrghm  13795  zndvds  14382  znleval  14386  znleval2  14387  isbasis3g  14489  lmfval  14635  lmbr  14656  lmbr2  14657  xmeterval  14878  xmeter  14879  cnbl0  14977  cnblcld  14978  limcrcl  15101  gausslemma2dlem1a  15506  bd3an  15728