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  2748  3reeanv  2779  ceqsex3v  2897  ceqsex4v  2898  ceqsex8v  2900  elin3  3447  raltpg  3777  tpss  3871  sikexlem  4295  dfpw12  4301  srelk  4524  br1stg  4730  elswap  4740  rabxp  4814  brinxp2  4835  brinxp  4836  brswap2  4860  dff1o3  5292  f1orn  5296  dff1o6  5475  oprabid  5550  eloprabga  5578  ndmovass  5618  dmpprod  5840  trrd  5925  porta  5933  lecex  6115  ovcelem1  6171  sbthlem3  6205  addccan2nclem1  6263  nmembers1lem1  6268  spacvallem1  6281  nchoicelem17  6305