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

Step	Hyp	Ref	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  90  najaii  91  najari  92  janaii  96  janaiii  97  janairi  98  jei  120  jeri  121  jai  146  jari  147  joi  161  jori  162  sei  169  seri  170  se-dual  172  se-dual-l  173  se-dual-r  174  se-ganaii  175  se-ganair  176  dui  198  duri  200  ceihi  208  jonaii  236  jonairi  237  nomei-gaiho  251  pameii  254  pameiii  255  gripaui  259  gripauri  260  gripauiis  262  gripau-trans  265  bckaji  269  ckinii  276  ckiniri  277  simsai  284  simsail  285  simsair  286  simsari  287  simsarii  288  mintui  300  minturi  301  mintu-sym  303  simsa-mintu  305  stecii  308  steciri  309  stecirii  310  muplii  313  muplili  314  mupliiri  315  mupliri  316  muplirii  317  simxui  320  simxuri  321  cei  334  ceri  335  ceri-lin  336  ceri-rin  337  subi  351  sub1  352  subeq-lem1  353  subeq-lem2  354  subid  355  zilcmi-nomei  368  cmima-zilcmi  369  kampui  385  kampuri  386  johei  389  joheri  390  kuhai  393  kuhari  394  niblii  411  nibliri  413  fahui  428  fahuil  429  fahuir  430  fahuri  431  taknii  438  kinfiri  441  kinrari  444  pa-dai  456  pa-dari  457  sezni-elt  468  baihei-inj  474  succ-zero-ref  478  succ-succi  489  nat-indi  491  nat-indii  492  nat-ind-cur  493  sumji-no  501  pilji-no  508  gt-zero-ref  512  kazmi-funii  523  pagbu-antisym  529  pagbu-trans  531  jompaui  536  jompauri  537  kuzypaui  540  kuzypauri  541  kihirnihi-refl  566  fancui  575  fancuii  576  mapti-ckini  581

Copyright terms: Public domain

W3C validator