Definition df-3an 936

Description: Define conjunction ('and') of three 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 630. (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 934	. 2 wff (ph /\ ps /\ ch)
5	1, 2	wa 358	. . 3 wff (ph /\ ps)
6	5, 3	wa 358	. 2 wff ((ph /\ ps) /\ ch)
7	4, 6	wb 176	1 wff ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))

This definition is referenced by:  3anass  938  3anrot  939  3ancoma  941  3anan32  946  3anor  948  3ioran  950  3simpa  952  3pm3.2i  1130  pm3.2an3  1131  3jca  1132  3anbi123i  1140  3imp  1145  3anbi123d  1252  3anim123d  1259  an6  1261  cadan  1392  19.26-3an  1595  nf3and  1823  nf3an  1827  hb3anOLD  1831  eeeanv  1914  sb3an  2070  mopick2  2271  r19.26-3  2749  3reeanv  2780  ceqsex3v  2898  ceqsex4v  2899  ceqsex8v  2901  elin3  3448  raltpg  3778  tpss  3872  sikexlem  4296  dfpw12  4302  srelk  4525  br1stg  4731  elswap  4741  rabxp  4815  brinxp2  4836  brinxp  4837  brswap2  4861  dff1o3  5293  f1orn  5297  dff1o6  5476  oprabid  5551  eloprabga  5579  ndmovass  5619  dmpprod  5841  trrd  5926  porta  5934  lecex  6116  ovcelem1  6172  sbthlem3  6206  addccan2nclem1  6264  nmembers1lem1  6269  spacvallem1  6282  nchoicelem17  6306