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  100  najaii  101  najari  102  janaii  106  janaiii  107  janairi  108  jei  130  jeri  131  jai  160  jari  161  joi  175  jori  176  sei  183  seri  184  se-dual  186  se-dual-l  187  se-dual-r  188  se-ganaii  189  se-ganair  190  dui  216  duri  218  du-sym-ganai  224  du-sym-go  225  ceihi  232  jonaii  272  jonairi  273  nomei-gaiho  288  pameii  291  pameiii  292  gripaui  296  gripauri  297  gripauiis  299  gripau-trans  302  bckaji  306  ckinii  313  ckiniri  314  simsai  321  simsail  322  simsair  323  simsari  324  simsarii  325  mintui  337  minturi  338  mintu-sym  340  simsa-mintu  342  stecii  345  steciri  346  stecirii  347  muplii  350  muplili  351  mupliiri  352  mupliri  353  muplirii  354  simxui  357  simxuri  358  cei  371  ceri  372  ceri-lin  373  ceri-rin  374  subi  390  sub1  391  subeq-lem1  392  subeq-lem2  393  subid  394  zilcmi-nomei  409  cmima-zilcmi  410  kampui  427  kampuri  428  johei  431  joheri  432  kuhai  435  kuhari  436  niblii  455  nibliri  457  fahui  472  fahuil  473  fahuir  474  fahuri  475  taknii  482  kinfiri  485  kinrari  488  pa-dai  500  pa-dari  501  sezni-elt  514  baihei-inj  520  succ-zero-ref  524  succ-succi  535  nat-indi  537  nat-indii  538  nat-ind-cur  539  sumji-no  547  pilji-no  554  gt-zero-ref  558  kazmi-funii  569  pagbu-antisym  575  pagbu-trans  577  jompaui  582  jompauri  583  kuzypaui  586  kuzypauri  587  kihirnihi-refl  612  fancui  632  fancuii  633  mapti-ckini  638
  Copyright terms: Public domain W3C validator