Definition df-3an 1004

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 1002	. 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  1006  3anrot  1007  3ancoma  1009  3anan32  1013  3ioran  1017  3simpa  1018  3pm3.2i  1199  pm3.2an3  1200  3jca  1201  3anbi123i  1212  3imp  1217  3anbi123d  1346  3anim123d  1353  an6  1355  19.26-3an  1529  hb3an  1596  nf3an  1612  nf3and  1615  eeeanv  1984  sb3an  2009  mopick2  2161  r19.26-3  2661  3reeanv  2702  ceqsex3v  2844  ceqsex4v  2845  ceqsex8v  2847  sbc3an  3091  elin3  3396  rexdifpr  3695  raltpg  3720  tpss  3839  dfopg  3858  opeq1  3860  opeq2  3861  opm  4324  otth2  4331  poirr  4402  po3nr  4405  wepo  4454  wetrep  4455  rabxp  4761  brinxp2  4791  brinxp  4792  sotri2  5132  sotri3  5133  f1orn  5590  dff1o6  5912  isosolem  5960  oprabid  6045  caovimo  6211  elovmpo  6216  elovmporab  6217  elovmporab1w  6218  dfxp3  6354  nnaord  6672  fiintim  7116  prmuloc  7776  ltrelxr  8230  rexuz2  9805  ltxr  10000  elixx3g  10126  elioo4g  10159  elioopnf  10192  elioomnf  10193  elicopnf  10194  elxrge0  10203  divelunit  10227  elfz2  10240  elfzuzb  10244  uzsplit  10317  fznn0  10338  elfzmlbp  10357  elfzo2  10375  fzolb2  10380  fzouzsplit  10406  ssfzo12bi  10460  fzind2  10475  dfrp2  10513  ccatsymb  11169  swrdsbslen  11237  swrdspsleq  11238  swrdccatin2  11300  pfxccatin12lem2  11302  pfxccatin12lem3  11303  pfxccatin12  11304  pfxccat3a  11309  abs2dif  11657  sumeq2  11910  divalgb  12476  bitsval2  12495  divgcdz  12532  rplpwr  12588  nnwosdc  12600  cncongr1  12665  pythagtriplem2  12829  pythagtrip  12846  xpscf  13420  issgrpd  13485  issubm2  13546  issubg3  13769  resgrpisgrp  13772  eqgval  13800  eqger  13801  eqgabl  13907  qusecsub  13908  rnglz  13948  rngpropd  13958  ringpropd  14041  ringrghm  14065  zndvds  14653  znleval  14657  znleval2  14658  isbasis3g  14760  lmfval  14907  lmbr  14927  lmbr2  14928  xmeterval  15149  xmeter  15150  cnbl0  15248  cnblcld  15249  limcrcl  15372  gausslemma2dlem1a  15777  umgr2edg1  16048  upgriswlkdc  16157  clwwlknon2x  16230  bd3an  16361