bb - brismu bridi

	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 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 ceihi 268 jonaii 309 jonairi 310 nomei-gaiho 325 pameii 328 pameiii 329 gripaui 333 gripauri 334 gripauiis 336 gripau-trans 339 bckaji 343 ckinii 350 ckiniri 351 simsai 358 simsail 359 simsair 360 simsari 361 simsarii 362 mintui 374 minturi 375 mintu-sym 377 simsa-mintu 379 stecii 382 steciri 383 stecirii 384 muplii 387 muplili 388 mupliiri 389 mupliri 390 muplirii 391 simxui 394 simxuri 395 cei 408 ceri 409 ceri-lin 410 ceri-rin 411 subi 448 sub1 449 subeq-lem1 450 subeq-lem2 451 subid 452 equs4 453 sub2 454 stdpc4 455 subh 456 zilcmi-nomei 461 cmima-zilcmi 462 kampui 479 kampuri 480 johei 483 joheri 484 kuhai 487 kuhari 488 niblii 507 nibliri 509 fahui 524 fahuil 525 fahuir 526 fahuri 527 taknii 535 kinfiri 538 kinrari 541 pa-dai 553 pa-dari 554 pomboi 561 pombori 562 sezni-elt 571 baihei-inj 578 succ-zero-ref 582 succ-succi 593 nat-indi 595 nat-indii 596 nat-ind-cur 597 sumji-no 605 pilji-no 612 gt-zero-ref 616 kazmi-funii 627 pagbu-antisym 633 pagbu-trans 635 jompaui 640 jompauri 641 kuzypaui 644 kuzypauri 645 kihirnihi-refl 679 kihirduhi-refl 684 kihirnihi-antisym 685 fancui 703 fancuii 704 mapti-ckini 709

Copyright terms: Public domain