HomeTheorem List (p. 8 of 9)
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List
| Home |
brismu
bridi Theorem List (p. 8 of 9) |
< Previous Next >
|
|
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List | ||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Syntax | sbtujli 701 |
|
| selbri tujli | ||
| Syntax | sbxanto 702 |
|
| selbri xanto | ||
| Syntax | sbxarju 703 |
|
| selbri xarju | ||
| Syntax | sbxasli 704 |
|
| selbri xasli | ||
| Syntax | sbxirma 705 |
|
| selbri xirma | ||
| Syntax | sbxruba 706 |
|
| selbri xruba | ||
| Syntax | sbxruki 707 |
|
| selbri xruki | ||
| Axiom | ax-skaselbri-blabi 708 | Automatically generated axiom: {blabi} is {skaselbri} |
| ⊢ skaselbri blabi | ||
| Axiom | ax-skaselbri-blanu 709 | Automatically generated axiom: {blanu} is {skaselbri} |
| ⊢ skaselbri blanu | ||
| Axiom | ax-skaselbri-bunre 710 | Automatically generated axiom: {bunre} is {skaselbri} |
| ⊢ skaselbri bunre | ||
| Axiom | ax-skaselbri-cicna 711 | Automatically generated axiom: {cicna} is {skaselbri} |
| ⊢ skaselbri cicna | ||
| Axiom | ax-skaselbri-crino 712 | Automatically generated axiom: {crino} is {skaselbri} |
| ⊢ skaselbri crino | ||
| Axiom | ax-skaselbri-grusi 713 | Automatically generated axiom: {grusi} is {skaselbri} |
| ⊢ skaselbri grusi | ||
| Axiom | ax-skaselbri-labyxuhe 714 | Automatically generated axiom: {labyxu'e} is {skaselbri} |
| ⊢ skaselbri labyxu'e | ||
| Axiom | ax-skaselbri-narju 715 | Automatically generated axiom: {narju} is {skaselbri} |
| ⊢ skaselbri narju | ||
| Axiom | ax-skaselbri-nukni 716 | Automatically generated axiom: {nukni} is {skaselbri} |
| ⊢ skaselbri nukni | ||
| Axiom | ax-skaselbri-pelxu 717 | Automatically generated axiom: {pelxu} is {skaselbri} |
| ⊢ skaselbri pelxu | ||
| Axiom | ax-skaselbri-xekri 718 | Automatically generated axiom: {xekri} is {skaselbri} |
| ⊢ skaselbri xekri | ||
| Axiom | ax-skaselbri-xunblabi 719 | Automatically generated axiom: {xunblabi} is {skaselbri} |
| ⊢ skaselbri xunblabi | ||
| Axiom | ax-skaselbri-xunre 720 | Automatically generated axiom: {xunre} is {skaselbri} |
| ⊢ skaselbri xunre | ||
| Axiom | ax-skaselbri-zirpu 721 | Automatically generated axiom: {zirpu} is {skaselbri} |
| ⊢ skaselbri zirpu | ||
| Axiom | ax-kluselbri-baxso 722 | Automatically generated axiom: {baxso} is {kluselbri} |
| ⊢ kluselbri baxso | ||
| Axiom | ax-kluselbri-bengo 723 | Automatically generated axiom: {bengo} is {kluselbri} |
| ⊢ kluselbri bengo | ||
| Axiom | ax-kluselbri-bemro 724 | Automatically generated axiom: {bemro} is {kluselbri} |
| ⊢ kluselbri bemro | ||
| Axiom | ax-kluselbri-bindo 725 | Automatically generated axiom: {bindo} is {kluselbri} |
| ⊢ kluselbri bindo | ||
| Axiom | ax-kluselbri-brazo 726 | Automatically generated axiom: {brazo} is {kluselbri} |
| ⊢ kluselbri brazo | ||
| Axiom | ax-kluselbri-brito 727 | Automatically generated axiom: {brito} is {kluselbri} |
| ⊢ kluselbri brito | ||
| Axiom | ax-kluselbri-budjo 728 | Automatically generated axiom: {budjo} is {kluselbri} |
| ⊢ kluselbri budjo | ||
| Axiom | ax-kluselbri-dadjo 729 | Automatically generated axiom: {dadjo} is {kluselbri} |
| ⊢ kluselbri dadjo | ||
| Axiom | ax-kluselbri-dotco 730 | Automatically generated axiom: {dotco} is {kluselbri} |
| ⊢ kluselbri dotco | ||
| Axiom | ax-kluselbri-dzipo 731 | Automatically generated axiom: {dzipo} is {kluselbri} |
| ⊢ kluselbri dzipo | ||
| Axiom | ax-kluselbri-filso 732 | Automatically generated axiom: {filso} is {kluselbri} |
| ⊢ kluselbri filso | ||
| Axiom | ax-kluselbri-fraso 733 | Automatically generated axiom: {fraso} is {kluselbri} |
| ⊢ kluselbri fraso | ||
| Axiom | ax-kluselbri-friko 734 | Automatically generated axiom: {friko} is {kluselbri} |
| ⊢ kluselbri friko | ||
| Axiom | ax-kluselbri-gento 735 | Automatically generated axiom: {gento} is {kluselbri} |
| ⊢ kluselbri gento | ||
| Axiom | ax-kluselbri-glico 736 | Automatically generated axiom: {glico} is {kluselbri} |
| ⊢ kluselbri glico | ||
| Axiom | ax-kluselbri-jegvo 737 | Automatically generated axiom: {jegvo} is {kluselbri} |
| ⊢ kluselbri jegvo | ||
| Axiom | ax-kluselbri-jerxo 738 | Automatically generated axiom: {jerxo} is {kluselbri} |
| ⊢ kluselbri jerxo | ||
| Axiom | ax-kluselbri-jordo 739 | Automatically generated axiom: {jordo} is {kluselbri} |
| ⊢ kluselbri jordo | ||
| Axiom | ax-kluselbri-jungo 740 | Automatically generated axiom: {jungo} is {kluselbri} |
| ⊢ kluselbri jungo | ||
| Axiom | ax-kluselbri-kadno 741 | Automatically generated axiom: {kadno} is {kluselbri} |
| ⊢ kluselbri kadno | ||
| Axiom | ax-kluselbri-ketco 742 | Automatically generated axiom: {ketco} is {kluselbri} |
| ⊢ kluselbri ketco | ||
| Axiom | ax-kluselbri-kisto 743 | Automatically generated axiom: {kisto} is {kluselbri} |
| ⊢ kluselbri kisto | ||
| Axiom | ax-kluselbri-latmo 744 | Automatically generated axiom: {latmo} is {kluselbri} |
| ⊢ kluselbri latmo | ||
| Axiom | ax-kluselbri-libjo 745 | Automatically generated axiom: {libjo} is {kluselbri} |
| ⊢ kluselbri libjo | ||
| Axiom | ax-kluselbri-lojbo 746 | Automatically generated axiom: {lojbo} is {kluselbri} |
| ⊢ kluselbri lojbo | ||
| Axiom | ax-kluselbri-lubno 747 | Automatically generated axiom: {lubno} is {kluselbri} |
| ⊢ kluselbri lubno | ||
| Axiom | ax-kluselbri-meljo 748 | Automatically generated axiom: {meljo} is {kluselbri} |
| ⊢ kluselbri meljo | ||
| Axiom | ax-kluselbri-merko 749 | Automatically generated axiom: {merko} is {kluselbri} |
| ⊢ kluselbri merko | ||
| Axiom | ax-kluselbri-mexco 750 | Automatically generated axiom: {mexco} is {kluselbri} |
| ⊢ kluselbri mexco | ||
| Axiom | ax-kluselbri-misro 751 | Automatically generated axiom: {misro} is {kluselbri} |
| ⊢ kluselbri misro | ||
| Axiom | ax-kluselbri-morko 752 | Automatically generated axiom: {morko} is {kluselbri} |
| ⊢ kluselbri morko | ||
| Axiom | ax-kluselbri-muslo 753 | Automatically generated axiom: {muslo} is {kluselbri} |
| ⊢ kluselbri muslo | ||
| Axiom | ax-kluselbri-polno 754 | Automatically generated axiom: {polno} is {kluselbri} |
| ⊢ kluselbri polno | ||
| Axiom | ax-kluselbri-ponjo 755 | Automatically generated axiom: {ponjo} is {kluselbri} |
| ⊢ kluselbri ponjo | ||
| Axiom | ax-kluselbri-porto 756 | Automatically generated axiom: {porto} is {kluselbri} |
| ⊢ kluselbri porto | ||
| Axiom | ax-kluselbri-rakso 757 | Automatically generated axiom: {rakso} is {kluselbri} |
| ⊢ kluselbri rakso | ||
| Axiom | ax-kluselbri-ropno 758 | Automatically generated axiom: {ropno} is {kluselbri} |
| ⊢ kluselbri ropno | ||
| Axiom | ax-kluselbri-rusko 759 | Automatically generated axiom: {rusko} is {kluselbri} |
| ⊢ kluselbri rusko | ||
| Axiom | ax-kluselbri-sadjo 760 | Automatically generated axiom: {sadjo} is {kluselbri} |
| ⊢ kluselbri sadjo | ||
| Axiom | ax-kluselbri-semto 761 | Automatically generated axiom: {semto} is {kluselbri} |
| ⊢ kluselbri semto | ||
| Axiom | ax-kluselbri-sirxo 762 | Automatically generated axiom: {sirxo} is {kluselbri} |
| ⊢ kluselbri sirxo | ||
| Axiom | ax-kluselbri-skoto 763 | Automatically generated axiom: {skoto} is {kluselbri} |
| ⊢ kluselbri skoto | ||
| Axiom | ax-kluselbri-softo 764 | Automatically generated axiom: {softo} is {kluselbri} |
| ⊢ kluselbri softo | ||
| Axiom | ax-kluselbri-spano 765 | Automatically generated axiom: {spano} is {kluselbri} |
| ⊢ kluselbri spano | ||
| Axiom | ax-kluselbri-sralo 766 | Automatically generated axiom: {sralo} is {kluselbri} |
| ⊢ kluselbri sralo | ||
| Axiom | ax-kluselbri-srito 767 | Automatically generated axiom: {srito} is {kluselbri} |
| ⊢ kluselbri srito | ||
| Axiom | ax-kluselbri-xazdo 768 | Automatically generated axiom: {xazdo} is {kluselbri} |
| ⊢ kluselbri xazdo | ||
| Axiom | ax-kluselbri-xebro 769 | Automatically generated axiom: {xebro} is {kluselbri} |
| ⊢ kluselbri xebro | ||
| Axiom | ax-kluselbri-xelso 770 | Automatically generated axiom: {xelso} is {kluselbri} |
| ⊢ kluselbri xelso | ||
| Axiom | ax-kluselbri-xindo 771 | Automatically generated axiom: {xindo} is {kluselbri} |
| ⊢ kluselbri xindo | ||
| Axiom | ax-kluselbri-xispo 772 | Automatically generated axiom: {xispo} is {kluselbri} |
| ⊢ kluselbri xispo | ||
| Axiom | ax-kluselbri-xrabo 773 | Automatically generated axiom: {xrabo} is {kluselbri} |
| ⊢ kluselbri xrabo | ||
| Axiom | ax-kluselbri-xriso 774 | Automatically generated axiom: {xriso} is {kluselbri} |
| ⊢ kluselbri xriso | ||
| Axiom | ax-kluselbri-xurdo 775 | Automatically generated axiom: {xurdo} is {kluselbri} |
| ⊢ kluselbri xurdo | ||
| Axiom | ax-since-respa 776 | Automatically generated axiom: {since} is a subrelation of {respa} |
| ⊢ 1 ka ce'u since ce'u ki'irni'i 1 ka ce'u respa ce'u | ||
| Axiom | ax-respa-danlu 777 | Automatically generated axiom: {respa} is a subrelation of {danlu} |
| ⊢ 1 ka ce'u respa ce'u ki'irni'i 1 ka ce'u danlu ce'u | ||
| Axiom | ax-remna-smani 778 | Automatically generated axiom: {remna} is a subrelation of {smani} |
| ⊢ 1 ka ce'u remna ce'u ki'irni'i 1 ka ce'u smani ce'u | ||
| Axiom | ax-smani-mabru 779 | Automatically generated axiom: {smani} is a subrelation of {mabru} |
| ⊢ 1 ka ce'u smani ce'u ki'irni'i 1 ka ce'u mabru ce'u | ||
| Axiom | ax-tirxu-mlatu 780 | Automatically generated axiom: {tirxu} is a subrelation of {mlatu} |
| ⊢ 1 ka ce'u tirxu ce'u ki'irni'i 1 ka ce'u mlatu ce'u | ||
| Axiom | ax-cinfo-mlatu 781 | Automatically generated axiom: {cinfo} is a subrelation of {mlatu} |
| ⊢ 1 ka ce'u cinfo ce'u ki'irni'i 1 ka ce'u mlatu ce'u | ||
| Axiom | ax-mlatu-mabru 782 | Automatically generated axiom: {mlatu} is a subrelation of {mabru} |
| ⊢ 1 ka ce'u mlatu ce'u ki'irni'i 1 ka ce'u mabru ce'u | ||
| Axiom | ax-xanto-mabru 783 | Automatically generated axiom: {xanto} is a subrelation of {mabru} |
| ⊢ 1 ka ce'u xanto ce'u ki'irni'i 1 ka ce'u mabru ce'u | ||
| Axiom | ax-xasli-mabru 784 | Automatically generated axiom: {xasli} is a subrelation of {mabru} |
| ⊢ 1 ka ce'u xasli ce'u ki'irni'i 1 ka ce'u mabru ce'u | ||
| Axiom | ax-xirma-mabru 785 | Automatically generated axiom: {xirma} is a subrelation of {mabru} |
| ⊢ 1 ka ce'u xirma ce'u ki'irni'i 1 ka ce'u mabru ce'u | ||
| Axiom | ax-xarju-mabru 786 | Automatically generated axiom: {xarju} is a subrelation of {mabru} |
| ⊢ 1 ka ce'u xarju ce'u ki'irni'i 1 ka ce'u mabru ce'u | ||
| Axiom | ax-ractu-mabru 787 | Automatically generated axiom: {ractu} is a subrelation of {mabru} |
| ⊢ 1 ka ce'u ractu ce'u ki'irni'i 1 ka ce'u mabru ce'u | ||
| Axiom | ax-smacu-mabru 788 | Automatically generated axiom: {smacu} is a subrelation of {mabru} |
| ⊢ 1 ka ce'u smacu ce'u ki'irni'i 1 ka ce'u mabru ce'u | ||
| Axiom | ax-kumte-mabru 789 | Automatically generated axiom: {kumte} is a subrelation of {mabru} |
| ⊢ 1 ka ce'u kumte ce'u ki'irni'i 1 ka ce'u mabru ce'u | ||
| Axiom | ax-mirli-mabru 790 | Automatically generated axiom: {mirli} is a subrelation of {mabru} |
| ⊢ 1 ka ce'u mirli ce'u ki'irni'i 1 ka ce'u mabru ce'u | ||
| Axiom | ax-cribe-mabru 791 | Automatically generated axiom: {cribe} is a subrelation of {mabru} |
| ⊢ 1 ka ce'u cribe ce'u ki'irni'i 1 ka ce'u mabru ce'u | ||
| Axiom | ax-ratcu-mabru 792 | Automatically generated axiom: {ratcu} is a subrelation of {mabru} |
| ⊢ 1 ka ce'u ratcu ce'u ki'irni'i 1 ka ce'u mabru ce'u | ||
| Axiom | ax-labno-gerku 793 | Automatically generated axiom: {labno} is a subrelation of {gerku} |
| ⊢ 1 ka ce'u labno ce'u ki'irni'i 1 ka ce'u gerku ce'u | ||
| Axiom | ax-lorxu-gerku 794 | Automatically generated axiom: {lorxu} is a subrelation of {gerku} |
| ⊢ 1 ka ce'u lorxu ce'u ki'irni'i 1 ka ce'u gerku ce'u | ||
| Axiom | ax-gerku-mabru 795 | Automatically generated axiom: {gerku} is a subrelation of {mabru} |
| ⊢ 1 ka ce'u gerku ce'u ki'irni'i 1 ka ce'u mabru ce'u | ||
| Axiom | ax-banfi-danlu 796 | Automatically generated axiom: {banfi} is a subrelation of {danlu} |
| ⊢ 1 ka ce'u banfi ce'u ki'irni'i 1 ka ce'u danlu ce'u | ||
| Axiom | ax-finpe-danlu 797 | Automatically generated axiom: {finpe} is a subrelation of {danlu} |
| ⊢ 1 ka ce'u finpe ce'u ki'irni'i 1 ka ce'u danlu ce'u | ||
| Axiom | ax-curnu-danlu 798 | Automatically generated axiom: {curnu} is a subrelation of {danlu} |
| ⊢ 1 ka ce'u curnu ce'u ki'irni'i 1 ka ce'u danlu ce'u | ||
| Axiom | ax-gunse-cipni 799 | Automatically generated axiom: {gunse} is a subrelation of {cipni} |
| ⊢ 1 ka ce'u gunse ce'u ki'irni'i 1 ka ce'u cipni ce'u | ||
| Axiom | ax-jipci-cipni 800 | Automatically generated axiom: {jipci} is a subrelation of {cipni} |
| ⊢ 1 ka ce'u jipci ce'u ki'irni'i 1 ka ce'u cipni ce'u | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |