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  du-syms  262  ceihi  269  jonaii  310  jonairi  311  nomei-gaiho  326  pameii  329  pameiii  330  gripaui  334  gripauri  335  gripauiis  337  gripau-trans  340  bckaji  344  ckinii  351  ckiniri  352  simsai  359  simsail  360  simsair  361  simsari  362  simsarii  363  simsa-sym  364  mintui  376  minturi  377  mintu-sym  379  simsa-mintu  381  stecii  384  steciri  385  stecirii  386  muplii  389  muplili  390  mupliiri  391  mupliri  392  muplirii  393  simxui  396  simxuri  397  cei  410  ceri  411  ceri-lin  412  ceri-rin  413  subi  450  sub1  451  subeq-lem1  452  subeq-lem2  453  subid  454  equs4  455  sub2  456  subequ2  457  stdpc4  458  stdpc6  459  subh  461  zilcmi-nomei  466  cmima-zilcmi  467  selcmi-zilcmi  468  kampui  485  kampuri  486  johei  489  joheri  490  kuhai  493  kuhari  494  niblii  513  nibliri  515  fahui  530  fahuil  531  fahuir  532  fahuri  533  taknii  541  kinfiri  544  kinrari  547  pa-dai  559  pa-dari  560  pomboi  567  pombori  568  sezni-elt  577  baihei-inj  584  succ-zero-ref  588  succ-succi  599  nat-indi  601  nat-indii  602  nat-ind-cur  603  sumji-no  611  pilji-no  618  gt-zero-ref  622  kazmi-funii  635  pagbu-antisym  646  pagbu-trans  648  jompaui  653  jompauri  654  kuzypaui  657  kuzypauri  658  kihirnihi-refl  692  kihirduhi-refl  697  kihirnihi-antisym  698  frinynahu-kacnahul  707  frinynahu-kacnahur  708  fancui  730  fancuii  731  mapti-ckini  736
  Copyright terms: Public domain W3C validator