Definition df-3an 932

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 396. (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 930	. 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  934  3anrot  935  3ancoma  937  3anan32  941  3ioran  945  3simpa  946  3pm3.2i  1127  pm3.2an3  1128  3jca  1129  3anbi123i  1138  3imp  1143  3anbi123d  1258  3anim123d  1265  an6  1267  19.26-3an  1427  hb3an  1497  nf3an  1513  nf3and  1516  eeeanv  1868  sb3an  1892  mopick2  2043  r19.26-3  2521  3reeanv  2559  ceqsex3v  2683  ceqsex4v  2684  ceqsex8v  2686  sbc3an  2922  elin3  3214  raltpg  3523  tpss  3632  dfopg  3650  opeq1  3652  opeq2  3653  opm  4094  otth2  4101  poirr  4167  po3nr  4170  wepo  4219  wetrep  4220  rabxp  4514  brinxp2  4544  brinxp  4545  sotri2  4872  sotri3  4873  f1orn  5311  dff1o6  5609  isosolem  5657  oprabid  5735  caovimo  5896  elovmpo  5903  dfxp3  6022  nnaord  6335  fiintim  6746  prmuloc  7275  ltrelxr  7697  rexuz2  9226  ltxr  9403  elixx3g  9525  elioo4g  9558  elioopnf  9591  elioomnf  9592  elicopnf  9593  elxrge0  9602  divelunit  9626  elfz2  9638  elfzuzb  9641  uzsplit  9713  fznn0  9734  elfzmlbp  9750  elfzo2  9768  fzolb2  9772  fzouzsplit  9797  ssfzo12bi  9843  fzind2  9857  abs2dif  10718  sumeq2  10967  divalgb  11417  divgcdz  11455  rplpwr  11508  cncongr1  11577  isbasis3g  11995  lmfval  12143  lmbr  12163  lmbr2  12164  xmeterval  12363  xmeter  12364  cnbl0  12456  cnblcld  12457  limcrcl  12509  bd3an  12609