Definition df-3an 969

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 399. (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 967	. 2 wff ( ph /\ ps /\ ch )
5	1, 2	wa 103	. . 3 wff ( ph /\ ps )
6	5, 3	wa 103	. 2 wff ( ( ph /\ ps ) /\ ch )
7	4, 6	wb 104	1 wff ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )

This definition is referenced by:  3anass  971  3anrot  972  3ancoma  974  3anan32  978  3ioran  982  3simpa  983  3pm3.2i  1164  pm3.2an3  1165  3jca  1166  3anbi123i  1177  3imp  1182  3anbi123d  1301  3anim123d  1308  an6  1310  19.26-3an  1470  hb3an  1537  nf3an  1553  nf3and  1556  eeeanv  1920  sb3an  1945  mopick2  2096  r19.26-3  2594  3reeanv  2634  ceqsex3v  2763  ceqsex4v  2764  ceqsex8v  2766  sbc3an  3007  elin3  3308  rexdifpr  3598  raltpg  3623  tpss  3732  dfopg  3750  opeq1  3752  opeq2  3753  opm  4206  otth2  4213  poirr  4279  po3nr  4282  wepo  4331  wetrep  4332  rabxp  4635  brinxp2  4665  brinxp  4666  sotri2  4995  sotri3  4996  f1orn  5436  dff1o6  5738  isosolem  5786  oprabid  5865  caovimo  6026  elovmpo  6033  dfxp3  6154  nnaord  6468  fiintim  6885  prmuloc  7498  ltrelxr  7950  rexuz2  9510  ltxr  9702  elixx3g  9828  elioo4g  9861  elioopnf  9894  elioomnf  9895  elicopnf  9896  elxrge0  9905  divelunit  9929  elfz2  9942  elfzuzb  9945  uzsplit  10017  fznn0  10038  elfzmlbp  10057  elfzo2  10075  fzolb2  10079  fzouzsplit  10104  ssfzo12bi  10150  fzind2  10164  dfrp2  10189  abs2dif  11034  sumeq2  11286  divalgb  11847  divgcdz  11889  rplpwr  11945  cncongr1  12014  pythagtriplem2  12175  pythagtrip  12192  isbasis3g  12585  lmfval  12733  lmbr  12754  lmbr2  12755  xmeterval  12976  xmeter  12977  cnbl0  13075  cnblcld  13076  limcrcl  13168  bd3an  13547