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  410  cmima-zilcmi  411  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  510  baihei-inj  516  succ-zero-ref  520  succ-succi  531  nat-indi  533  nat-indii  534  nat-ind-cur  535  sumji-no  543  pilji-no  550  gt-zero-ref  554  kazmi-funii  565  pagbu-antisym  571  pagbu-trans  573  jompaui  578  jompauri  579  kuzypaui  582  kuzypauri  583  kihirnihi-refl  608  fancui  628  fancuii  629  mapti-ckini  634
  Copyright terms: Public domain W3C validator