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 348 bsimsa 356 simsai 358 simsari 361 bdunli 365 dunlii 367 dunliri 368 dunli-sym 370 bmintu 372 mintui 374 minturi 375 mintu-sym 377 stecii 382 steciri 383 muplii 387 muplili 388 mupliiri 389 mupliri 390 muplirii 391 simxui 394 simxuri 395 tei 398 teri 399 te-dual 401 te-dual-l 402 te-dual-r 403 te-ganaii 404 te-ganair 405 selbrii 498 selbriri 499 taknii 535 kinfiri 538 kinrari 541 sezni-elt 571 sumji-no 605 pilji-no 612 dugrii 621 dugriri 622 kihirnihi-refl 679 kihirduhi-refl 684 kihirnihi-antisym 685 fancui 703 fancuii 704 mapti-ckini 709