Definition df-3an 774

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 772	. 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 776  3anrot 777  3ancoma 779  3simpa 782  3pm3.2i 815  3jca 816  3anim123i 818  3anbi123i 819  3imp 824  3exp 829  3anbi123d 889  3anim123d 896  an6 898  hb3an 988  sb3an 1222  sbc3ang 1950  otthg 2757  poirr 2809  po3nr 2812  dfwe2 2898  wefrc 2906  brinxp 3194  f1orn 3637  f1ofv 3816  tz7.49c 3899  ndmoprass 3988  oaord 4119  fiint 4486  abfii2 4488  alephval3 4826  sup2 5949  elioo3g 6268  ioossicc 6281  rexuz2 6328  elfz2t 6355  elfzuzb 6359  fznn0t 6399  expword2it 6487  abs2dift 6790  climcmplem 7024  isumcmpi 7101  mulc1cncf 7165  infxpidmlem7 7452  isbasis3g 7506  bl2in 7731  lmfval 7811  iscauf 7825  iscau5 7826  sspval 8251  efifolem4 8553  eff1i 8578  axgroth3 8631  lediv2itALT 8638  symgoprab 8669  intn3an1d 8688  intn3an2d 8689  intn3an3d 8690  hmph 8762  dmhmph 8770  rnhmph 8771  hmeogrp 8776  efilcp 8795  efilcp2 8800  cnfilca 8801  ishoma 8909  ishomb 8910  hilcau 9217  dfadj2 9943  cnvadj 9947  adjeqt 9989  eleigvec2t 10012  irred 10443

Copyright terms: Public domain