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  453  nibliri  455  fahui  470  fahuil  471  fahuir  472  fahuri  473  taknii  480  kinfiri  483  kinrari  486  pa-dai  498  pa-dari  499  sezni-elt  512  baihei-inj  518  succ-zero-ref  522  succ-succi  533  nat-indi  535  nat-indii  536  nat-ind-cur  537  sumji-no  545  pilji-no  552  gt-zero-ref  556  kazmi-funii  567  pagbu-antisym  573  pagbu-trans  575  jompaui  580  jompauri  581  kuzypaui  584  kuzypauri  585  kihirnihi-refl  610  fancui  630  fancuii  631  mapti-ckini  636
  Copyright terms: Public domain W3C validator