Definition df-3an 775

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	⊢ ((φ ⋀ ψ ⋀ χ) ↔ ((φ ⋀ ψ) ⋀ χ))

Detailed syntax breakdown of Definition df-3an

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		wps	. . 3 wff ψ
3		wch	. . 3 wff χ
4	1, 2, 3	w3a 773	. 2 wff (φ ⋀ ψ ⋀ χ)
5	1, 2	wa 223	. . 3 wff (φ ⋀ ψ)
6	5, 3	wa 223	. 2 wff ((φ ⋀ ψ) ⋀ χ)
7	4, 6	wb 146	1 wff ((φ ⋀ ψ ⋀ χ) ↔ ((φ ⋀ ψ) ⋀ χ))

This definition is referenced by:  3anass 777  3anrot 778  3ancoma 780  3simpa 783  3pm3.2i 816  3jca 817  3anim123i 819  3anbi123i 820  3imp 825  3exp 830  3anbi123d 890  3anim123d 897  an6 899  hb3an 1009  sb3an 1233  sbc3ang 1969  otthg 2780  poirr 2836  po3nr 2839  dfwe2 2925  wefrc 2933  brinxp 3222  f1orn 3683  f1ofv 3862  tz7.49c 3945  ndmoprass 4034  oaord 4165  fiint 4534  abfii2 4536  alephval3 4875  sup2 5998  elioo3g 6317  ioossicc 6330  rexuz2 6377  elfz2t 6404  elfzuzb 6408  fznn0t 6448  expword2it 6536  abs2dift 6839  climcmplem 7073  isumcmpi 7150  mulc1cncf 7214  infxpidmlem7 7501  isbasis3g 7555  bl2in 7783  lmfval 7863  iscauf 7877  iscau5 7878  nvex 8169  isnv 8170  sspval 8316  efifolem4 8640  eff1i 8665  axgroth3 8718  h2hcau 8788  dfadj2 9729  cnvadj 9733  adjeqt 9775  eleigvec2t 9798  irred 10229  lediv2itALT 10276  symgoprab 10307  intn3an1d 10328  intn3an2d 10329  intn3an3d 10330  hmph 10411  dmhmph 10419  rnhmph 10420  hmeogrp 10425  efilcp 10445  efilcp2 10450  cnfilca 10451  ishoma 10559  ishomb 10560

Copyright terms: Public domain