HomeTheorem List (p. 8 of 8)
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List
| Home |
brismu
bridi Theorem List (p. 8 of 8) |
< Previous Wrap >
|
|
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List | ||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Axiom | ax-kluselbri-polno 701 | Automatically generated axiom: {polno} is {kluselbri} |
| ⊢ kluselbri polno | ||
| Axiom | ax-kluselbri-ponjo 702 | Automatically generated axiom: {ponjo} is {kluselbri} |
| ⊢ kluselbri ponjo | ||
| Axiom | ax-kluselbri-porto 703 | Automatically generated axiom: {porto} is {kluselbri} |
| ⊢ kluselbri porto | ||
| Axiom | ax-kluselbri-rakso 704 | Automatically generated axiom: {rakso} is {kluselbri} |
| ⊢ kluselbri rakso | ||
| Axiom | ax-kluselbri-ropno 705 | Automatically generated axiom: {ropno} is {kluselbri} |
| ⊢ kluselbri ropno | ||
| Axiom | ax-kluselbri-rusko 706 | Automatically generated axiom: {rusko} is {kluselbri} |
| ⊢ kluselbri rusko | ||
| Axiom | ax-kluselbri-sadjo 707 | Automatically generated axiom: {sadjo} is {kluselbri} |
| ⊢ kluselbri sadjo | ||
| Axiom | ax-kluselbri-semto 708 | Automatically generated axiom: {semto} is {kluselbri} |
| ⊢ kluselbri semto | ||
| Axiom | ax-kluselbri-sirxo 709 | Automatically generated axiom: {sirxo} is {kluselbri} |
| ⊢ kluselbri sirxo | ||
| Axiom | ax-kluselbri-skoto 710 | Automatically generated axiom: {skoto} is {kluselbri} |
| ⊢ kluselbri skoto | ||
| Axiom | ax-kluselbri-softo 711 | Automatically generated axiom: {softo} is {kluselbri} |
| ⊢ kluselbri softo | ||
| Axiom | ax-kluselbri-spano 712 | Automatically generated axiom: {spano} is {kluselbri} |
| ⊢ kluselbri spano | ||
| Axiom | ax-kluselbri-sralo 713 | Automatically generated axiom: {sralo} is {kluselbri} |
| ⊢ kluselbri sralo | ||
| Axiom | ax-kluselbri-srito 714 | Automatically generated axiom: {srito} is {kluselbri} |
| ⊢ kluselbri srito | ||
| Axiom | ax-kluselbri-xazdo 715 | Automatically generated axiom: {xazdo} is {kluselbri} |
| ⊢ kluselbri xazdo | ||
| Axiom | ax-kluselbri-xebro 716 | Automatically generated axiom: {xebro} is {kluselbri} |
| ⊢ kluselbri xebro | ||
| Axiom | ax-kluselbri-xelso 717 | Automatically generated axiom: {xelso} is {kluselbri} |
| ⊢ kluselbri xelso | ||
| Axiom | ax-kluselbri-xindo 718 | Automatically generated axiom: {xindo} is {kluselbri} |
| ⊢ kluselbri xindo | ||
| Axiom | ax-kluselbri-xispo 719 | Automatically generated axiom: {xispo} is {kluselbri} |
| ⊢ kluselbri xispo | ||
| Axiom | ax-kluselbri-xrabo 720 | Automatically generated axiom: {xrabo} is {kluselbri} |
| ⊢ kluselbri xrabo | ||
| Axiom | ax-kluselbri-xriso 721 | Automatically generated axiom: {xriso} is {kluselbri} |
| ⊢ kluselbri xriso | ||
| Axiom | ax-kluselbri-xurdo 722 | Automatically generated axiom: {xurdo} is {kluselbri} |
| ⊢ kluselbri xurdo | ||
| Axiom | ax-since-respa 723 | 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 724 | 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 725 | 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 726 | 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 727 | 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 728 | 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 729 | 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 730 | 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 731 | 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 732 | 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 733 | 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 734 | 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 735 | 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 736 | 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 737 | 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 738 | 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 739 | 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 740 | 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 741 | 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 742 | 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 743 | 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 744 | 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 745 | 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 746 | 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 747 | 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 | ||
| Axiom | ax-xruki-cipni 748 | Automatically generated axiom: {xruki} is a subrelation of {cipni} |
| ⊢ 1 ka ce'u xruki ce'u ki'irni'i 1 ka ce'u cipni ce'u | ||
| Axiom | ax-datka-cipni 749 | Automatically generated axiom: {datka} is a subrelation of {cipni} |
| ⊢ 1 ka ce'u datka ce'u ki'irni'i 1 ka ce'u cipni ce'u | ||
| Axiom | ax-cipni-danlu 750 | Automatically generated axiom: {cipni} is a subrelation of {danlu} |
| ⊢ 1 ka ce'u cipni ce'u ki'irni'i 1 ka ce'u danlu ce'u | ||
| Axiom | ax-toldi-cinki 751 | Automatically generated axiom: {toldi} is a subrelation of {cinki} |
| ⊢ 1 ka ce'u toldi ce'u ki'irni'i 1 ka ce'u cinki ce'u | ||
| Axiom | ax-jukni-cinki 752 | Automatically generated axiom: {jukni} is a subrelation of {cinki} |
| ⊢ 1 ka ce'u jukni ce'u ki'irni'i 1 ka ce'u cinki ce'u | ||
| Axiom | ax-manti-cinki 753 | Automatically generated axiom: {manti} is a subrelation of {cinki} |
| ⊢ 1 ka ce'u manti ce'u ki'irni'i 1 ka ce'u cinki ce'u | ||
| Axiom | ax-sfani-cinki 754 | Automatically generated axiom: {sfani} is a subrelation of {cinki} |
| ⊢ 1 ka ce'u sfani ce'u ki'irni'i 1 ka ce'u cinki ce'u | ||
| Axiom | ax-jalra-cinki 755 | Automatically generated axiom: {jalra} is a subrelation of {cinki} |
| ⊢ 1 ka ce'u jalra ce'u ki'irni'i 1 ka ce'u cinki ce'u | ||
| Axiom | ax-civla-cinki 756 | Automatically generated axiom: {civla} is a subrelation of {cinki} |
| ⊢ 1 ka ce'u civla ce'u ki'irni'i 1 ka ce'u cinki ce'u | ||
| Axiom | ax-bifce-cinki 757 | Automatically generated axiom: {bifce} is a subrelation of {cinki} |
| ⊢ 1 ka ce'u bifce ce'u ki'irni'i 1 ka ce'u cinki ce'u | ||
| Axiom | ax-cinki-danlu 758 | Automatically generated axiom: {cinki} is a subrelation of {danlu} |
| ⊢ 1 ka ce'u cinki ce'u ki'irni'i 1 ka ce'u danlu ce'u | ||
| Axiom | ax-lanme-bakni 759 | Automatically generated axiom: {lanme} is a subrelation of {bakni} |
| ⊢ 1 ka ce'u lanme ce'u ki'irni'i 1 ka ce'u bakni ce'u | ||
| Axiom | ax-kanba-bakni 760 | Automatically generated axiom: {kanba} is a subrelation of {bakni} |
| ⊢ 1 ka ce'u kanba ce'u ki'irni'i 1 ka ce'u bakni ce'u | ||
| Axiom | ax-bakni-mabru 761 | Automatically generated axiom: {bakni} is a subrelation of {mabru} |
| ⊢ 1 ka ce'u bakni ce'u ki'irni'i 1 ka ce'u mabru ce'u | ||
| Axiom | ax-mabru-danlu 762 | Automatically generated axiom: {mabru} is a subrelation of {danlu} |
| ⊢ 1 ka ce'u mabru ce'u ki'irni'i 1 ka ce'u danlu ce'u | ||
| Axiom | ax-xruba-spati 763 | Automatically generated axiom: {xruba} is a subrelation of {spati} |
| ⊢ 1 ka ce'u xruba ce'u ki'irni'i 1 ka ce'u spati ce'u | ||
| Axiom | ax-tujli-spati 764 | Automatically generated axiom: {tujli} is a subrelation of {spati} |
| ⊢ 1 ka ce'u tujli ce'u ki'irni'i 1 ka ce'u spati ce'u | ||
| Axiom | ax-srasu-spati 765 | Automatically generated axiom: {srasu} is a subrelation of {spati} |
| ⊢ 1 ka ce'u srasu ce'u ki'irni'i 1 ka ce'u spati ce'u | ||
| Axiom | ax-sluni-spati 766 | Automatically generated axiom: {sluni} is a subrelation of {spati} |
| ⊢ 1 ka ce'u sluni ce'u ki'irni'i 1 ka ce'u spati ce'u | ||
| Axiom | ax-rozgu-spati 767 | Automatically generated axiom: {rozgu} is a subrelation of {spati} |
| ⊢ 1 ka ce'u rozgu ce'u ki'irni'i 1 ka ce'u spati ce'u | ||
| Axiom | ax-poplu-spati 768 | Automatically generated axiom: {poplu} is a subrelation of {spati} |
| ⊢ 1 ka ce'u poplu ce'u ki'irni'i 1 ka ce'u spati ce'u | ||
| Axiom | ax-nimre-spati 769 | Automatically generated axiom: {nimre} is a subrelation of {spati} |
| ⊢ 1 ka ce'u nimre ce'u ki'irni'i 1 ka ce'u spati ce'u | ||
| Axiom | ax-marna-spati 770 | Automatically generated axiom: {marna} is a subrelation of {spati} |
| ⊢ 1 ka ce'u marna ce'u ki'irni'i 1 ka ce'u spati ce'u | ||
| Axiom | ax-lelxe-spati 771 | Automatically generated axiom: {lelxe} is a subrelation of {spati} |
| ⊢ 1 ka ce'u lelxe ce'u ki'irni'i 1 ka ce'u spati ce'u | ||
| Axiom | ax-ckunu-spati 772 | Automatically generated axiom: {ckunu} is a subrelation of {spati} |
| ⊢ 1 ka ce'u ckunu ce'u ki'irni'i 1 ka ce'u spati ce'u | ||
| Axiom | ax-cindu-spati 773 | Automatically generated axiom: {cindu} is a subrelation of {spati} |
| ⊢ 1 ka ce'u cindu ce'u ki'irni'i 1 ka ce'u spati ce'u | ||
| Axiom | ax-bambu-spati 774 | Automatically generated axiom: {bambu} is a subrelation of {spati} |
| ⊢ 1 ka ce'u bambu ce'u ki'irni'i 1 ka ce'u spati ce'u | ||
| < Previous Wrap > |
| Copyright terms: Public domain | < Previous Wrap > |