bt - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > bt

Theorem bt 6

Description: Normal form for ternary selbri. (Contributed by la korvo, 14-Aug-2023.)

**Assertion**
Ref	Expression
bt	bridi ko'a bu'a ko'e ko'i

**Proof of Theorem bt**
Step	Hyp	Ref	Expression
1		btb 3	1 bridi ko'a bu'a ko'e ko'i

Colors of variables: sumti selbri bridi

Syntax hints: tsb 1 tss 2 btb 3

This theorem is referenced by: bckini 349 bsimsa 357 simsai 359 simsari 362 simsa-sym 364 bdunli 366 dunlii 368 dunliri 369 dunli-sym 371 bmintu 374 mintui 376 minturi 377 mintu-sym 379 stecii 384 steciri 385 muplii 389 muplili 390 mupliiri 391 mupliri 392 muplirii 393 simxui 396 simxuri 397 tei 400 teri 401 te-dual 403 te-dual-l 404 te-dual-r 405 te-ganaii 406 te-ganair 407 selbrii 504 selbriri 505 taknii 541 kinfiri 544 kinrari 547 sezni-elt 577 sumji-no 611 pilji-no 618 dugrii 629 dugriri 630 kihirnihi-refl 692 kihirduhi-refl 697 kihirnihi-antisym 698 frinynahu-kacnahul 707 frinynahu-kacnahur 708 fancui 730 fancuii 731 mapti-ckini 736