Definition df-3an 777

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 439.

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 775	. 2 wff (ph /\ ps /\ ch)
5	1, 2	wa 223	. . 3 wff (ph /\ ps)
6	5, 3	wa 223	. 2 wff ((ph /\ ps) /\ ch)
7	4, 6	wb 146	1 wff ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))

This definition is referenced by:  3anass 779  3anrot 780  3ancoma 782  3simpa 785  3pm3.2i 818  3jca 819  3anim123i 821  3anbi123i 822  3imp 827  3exp 832  3anbi123d 893  3anim123d 900  an6 902  hb3an 1012  sb3an 1238  sbc3ang 1977  otthg 2788  poirr 2843  po3nr 2846  dfwe2 2933  wefrc 2941  brinxp 3230  f1orn 3696  f1ofv 3875  tz7.49c 3958  ndmoprass 4046  oaord 4179  fiint 4548  abfii2 4550  alephval3 4891  sup2 6019  elioo3g 6344  ioossicc 6357  rexuz2 6405  elfz2t 6432  elfzuzb 6436  fznn0t 6476  expword2it 6565  abs2dift 6860  climcmplem 7095  isumcmpi 7173  mulc1cncf 7237  infxpidmlem7 7515  isbasis3g 7570  bl2in 7800  lmfval 7882  iscauf 7896  iscau5 7898  iscaunns 7901  nvex 8187  isnv 8188  sspval 8339  efifolem4 8680  eff1i 8699  axgroth3 8734  h2hcau 8804  dfadj2 9767  cnvadj 9771  adjeqt 9814  eleigvec2t 9837  irred 10276  lediv2itALT 10326  symgoprab 10357  intn3an1d 10383  intn3an2d 10384  intn3an3d 10385  hmph 10466  dmhmph 10474  rnhmph 10475  hmeogrp 10480  efilcp 10500  efilcp2 10505  cnfilca 10506  ishoma 10627  ishomb 10628

Copyright terms: Public domain