Home brismu bridi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  bb

Theorem bb 5
Description: Normal form for binary selbri. (Contributed by la korvo, 14-Aug-2023.)
Assertion
Ref Expression
bb bridi ko'a bu'a ko'e

Proof of Theorem bb
StepHypRef Expression
1 btb 3 1 bridi ko'a bu'a ko'e
Colors of variables: sumti selbri bridi
Syntax hints:  tsb 1  tss 2  btb 3
This theorem is referenced by:  najai  122  najaii  123  najari  124  janaii  128  janaiii  129  janairi  130  jei  153  jeri  154  jai  191  jari  192  joi  206  jori  207  sei  214  seri  215  se-dual  217  se-dual-l  218  se-dual-r  219  se-ganaii  220  se-ganair  221  dui  252  duri  254  du-sym-ganai  260  du-sym-go  261  ceihi  268  jonaii  309  jonairi  310  nomei-gaiho  325  pameii  328  pameiii  329  gripaui  333  gripauri  334  gripauiis  336  gripau-trans  339  bckaji  343  ckinii  350  ckiniri  351  simsai  358  simsail  359  simsair  360  simsari  361  simsarii  362  mintui  374  minturi  375  mintu-sym  377  simsa-mintu  379  stecii  382  steciri  383  stecirii  384  muplii  387  muplili  388  mupliiri  389  mupliri  390  muplirii  391  simxui  394  simxuri  395  cei  408  ceri  409  ceri-lin  410  ceri-rin  411  subi  448  sub1  449  subeq-lem1  450  subeq-lem2  451  subid  452  equs4  453  sub2  454  stdpc4  455  subh  456  zilcmi-nomei  461  cmima-zilcmi  462  kampui  479  kampuri  480  johei  483  joheri  484  kuhai  487  kuhari  488  niblii  507  nibliri  509  fahui  524  fahuil  525  fahuir  526  fahuri  527  taknii  535  kinfiri  538  kinrari  541  pa-dai  553  pa-dari  554  pomboi  561  pombori  562  sezni-elt  571  baihei-inj  578  succ-zero-ref  582  succ-succi  593  nat-indi  595  nat-indii  596  nat-ind-cur  597  sumji-no  605  pilji-no  612  gt-zero-ref  616  kazmi-funii  627  pagbu-antisym  633  pagbu-trans  635  jompaui  640  jompauri  641  kuzypaui  644  kuzypauri  645  kihirnihi-refl  679  kihirduhi-refl  684  kihirnihi-antisym  685  fancui  703  fancuii  704  mapti-ckini  709
  Copyright terms: Public domain W3C validator