Definition df-3an 783

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

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

This definition is referenced by:  3anass 785  3anrot 786  3ancoma 788  3simpa 791  3pm3.2i 824  3jca 825  3anim123i 827  3anbi123i 828  3imp 833  3exp 838  3anbi123d 899  3anim123d 906  an6 908  hb3an 1048  sb3an 1275  sbc3ang 2027  otthg 2866  poirr 2923  po3nr 2926  wefrc 2970  dfwe2 3140  brinxp 3318  f1orn 3806  dff1o6 3991  ndmoprass 4109  tz7.49c 4261  oaord 4317  fiint 4703  abfii2 4705  alephval3 5053  sup2 6219  elioo3g 6506  eliooord 6514  rexuz2 6572  elfz2 6600  elfzuzb 6604  fznn0 6647  expword2i 6802  abs2dif 7105  climcmplem 7340  isumcmpii 7419  mulc1cncf 7484  infxpidmlem7 7770  isbasis3g 7825  bl2in 8053  lmfval 8136  iscauf 8150  iscau5 8152  iscaunns 8155  nvex 8477  isnv 8478  sspval 8636  efifolem4 8997  axgroth3 9051  h2hcau 9124  dfadj2 10092  cnvadj 10096  adjeq 10139  eleigvec2 10162  irredi 10603  lediv2aALT 10656  symgoprab 10687  intn3an1d 10713  intn3an2d 10714  intn3an3d 10715  hmph 11030  dmhmph 11038  rnhmph 11039  hmeogrp 11044  efilcp 11083  efilcp2 11087  cnfilca 11088  limfillem1 11101  ishoma 11242  ishomb 11243  3anor 11389  compfipin0 11493  dfcon2 11501  fbasfip 11627  fbunfip 11631  filssufillem 11655  flimff 11707  fclsfnflim 11726  flimfnfcls 11727  fclusff 11735  phtpcer 12104

Copyright terms: Public domain