Definition df-3an 981

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 979	. 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  983  3anrot  984  3ancoma  986  3anan32  990  3ioran  994  3simpa  995  3pm3.2i  1176  pm3.2an3  1177  3jca  1178  3anbi123i  1189  3imp  1194  3anbi123d  1322  3anim123d  1329  an6  1331  19.26-3an  1493  hb3an  1560  nf3an  1576  nf3and  1579  eeeanv  1943  sb3an  1968  mopick2  2119  r19.26-3  2617  3reeanv  2658  ceqsex3v  2791  ceqsex4v  2792  ceqsex8v  2794  sbc3an  3036  elin3  3338  rexdifpr  3632  raltpg  3657  tpss  3770  dfopg  3788  opeq1  3790  opeq2  3791  opm  4246  otth2  4253  poirr  4319  po3nr  4322  wepo  4371  wetrep  4372  rabxp  4675  brinxp2  4705  brinxp  4706  sotri2  5038  sotri3  5039  f1orn  5483  dff1o6  5790  isosolem  5838  oprabid  5920  caovimo  6082  elovmpo  6086  dfxp3  6209  nnaord  6524  fiintim  6942  prmuloc  7579  ltrelxr  8032  rexuz2  9595  ltxr  9789  elixx3g  9915  elioo4g  9948  elioopnf  9981  elioomnf  9982  elicopnf  9983  elxrge0  9992  divelunit  10016  elfz2  10029  elfzuzb  10033  uzsplit  10106  fznn0  10127  elfzmlbp  10146  elfzo2  10164  fzolb2  10168  fzouzsplit  10193  ssfzo12bi  10239  fzind2  10253  dfrp2  10278  abs2dif  11129  sumeq2  11381  divalgb  11944  divgcdz  11986  rplpwr  12042  nnwosdc  12054  cncongr1  12117  pythagtriplem2  12280  pythagtrip  12297  xpscf  12785  issgrpd  12837  issubm2  12886  issubg3  13092  resgrpisgrp  13095  eqgval  13123  eqger  13124  eqgabl  13222  qusecsub  13223  rnglz  13254  rngpropd  13264  ringpropd  13347  isbasis3g  13899  lmfval  14045  lmbr  14066  lmbr2  14067  xmeterval  14288  xmeter  14289  cnbl0  14387  cnblcld  14388  limcrcl  14480  bd3an  14935