Definition df-3an 1007

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 1005	. 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  1009  3anrot  1010  3ancoma  1012  3anan32  1016  3ioran  1020  3simpa  1021  3pm3.2i  1202  pm3.2an3  1203  3jca  1204  3anbi123i  1215  3imp  1220  3anbi123d  1349  3anim123d  1356  an6  1358  19.26-3an  1532  hb3an  1599  nf3an  1615  nf3and  1618  eeeanv  1989  sb3an  2014  mopick2  2166  r19.26-3  2675  3reeanv  2716  ceqsex3v  2859  ceqsex4v  2860  ceqsex8v  2862  sbc3an  3107  elin3  3414  rexdifpr  3722  raltpg  3747  tpss  3867  dfopg  3886  opeq1  3888  opeq2  3889  opm  4355  otth2  4362  poirr  4433  po3nr  4436  wepo  4485  wetrep  4486  rabxp  4792  brinxp2  4822  brinxp  4823  sotri2  5165  sotri3  5166  f1orn  5629  dff1o6  5955  isosolem  6003  oprabid  6090  caovimo  6256  elovmpo  6261  elovmporab  6262  elovmporab1w  6263  dfxp3  6403  nnaord  6755  fiintim  7204  prmuloc  7897  ltrelxr  8350  rexuz2  9931  ltxr  10127  elixx3g  10253  elioo4g  10286  elioopnf  10319  elioomnf  10320  elicopnf  10321  elxrge0  10330  divelunit  10354  elfz2  10368  elfzuzb  10372  uzsplit  10448  fznn0  10469  elfzmlbp  10488  elfzo2  10506  fzolb2  10511  fzouzsplit  10537  ssfzo12bi  10592  fzind2  10607  dfrp2  10647  ccatsymb  11315  swrdsbslen  11383  swrdspsleq  11384  swrdccatin2  11446  pfxccatin12lem2  11448  pfxccatin12lem3  11449  pfxccatin12  11450  pfxccat3a  11455  abs2dif  11816  sumeq2  12069  divalgb  12636  bitsval2  12655  divgcdz  12692  rplpwr  12748  nnwosdc  12760  cncongr1  12825  pythagtriplem2  12989  pythagtrip  13006  ballotfilemelo  13166  xpscf  13611  issgrpd  13675  issubm2  13728  issubg3  13945  resgrpisgrp  13948  eqgval  13976  eqger  13977  eqgabl  14083  qusecsub  14084  rnglz  14184  rngpropd  14194  ringpropd  14281  ringrghm  14305  zndvds  14923  znleval  14927  znleval2  14928  isbasis3g  15037  lmfval  15184  lmbr  15204  lmbr2  15205  xmeterval  15426  xmeter  15427  cnbl0  15525  cnblcld  15526  limcrcl  15649  gausslemma2dlem1a  16057  umgr2edg1  16330  subusgr  16396  upgriswlkdc  16481  clwwlknon2x  16556  bd3an  16726