HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Definition df-3an 776
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
StepHypRef Expression
1 wph . . 3 wff ph
2 wps . . 3 wff ps
3 wch . . 3 wff ch
41, 2, 3w3a 774 . 2 wff (ph /\ ps /\ ch)
51, 2wa 223 . . 3 wff (ph /\ ps)
65, 3wa 223 . 2 wff ((ph /\ ps) /\ ch)
74, 6wb 146 1 wff ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
Colors of variables: wff set class
This definition is referenced by:  3anass 778  3anrot 779  3ancoma 781  3simpa 784  3pm3.2i 817  3jca 818  3anim123i 820  3anbi123i 821  3imp 826  3exp 831  3anbi123d 891  3anim123d 898  an6 900  hb3an 1010  sb3an 1236  sbc3ang 1975  otthg 2785  poirr 2840  po3nr 2843  dfwe2 2930  wefrc 2938  brinxp 3227  f1orn 3689  f1ofv 3868  tz7.49c 3951  ndmoprass 4040  oaord 4171  fiint 4540  abfii2 4542  alephval3 4883  sup2 6006  elioo3g 6325  ioossicc 6338  rexuz2 6385  elfz2t 6412  elfzuzb 6416  fznn0t 6456  expword2it 6544  abs2dift 6847  climcmplem 7081  isumcmpi 7158  mulc1cncf 7222  infxpidmlem7 7509  isbasis3g 7563  bl2in 7795  lmfval 7877  iscauf 7891  iscau5 7893  nvex 8182  isnv 8183  sspval 8329  efifolem4 8659  eff1i 8683  axgroth3 8718  h2hcau 8788  dfadj2 9752  cnvadj 9756  adjeqt 9798  eleigvec2t 9821  irred 10258  lediv2itALT 10305  symgoprab 10336  intn3an1d 10364  intn3an2d 10365  intn3an3d 10366  hmph 10447  dmhmph 10455  rnhmph 10456  hmeogrp 10461  efilcp 10481  efilcp2 10486  cnfilca 10487  ishoma 10595  ishomb 10596
Copyright terms: Public domain