HomeTheorem List (p. 9 of 9)
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List
| Home |
brismu
bridi Theorem List (p. 9 of 9) |
< Previous Wrap >
|
|
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List | ||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Axiom | ax-xruki-cipni 801 | 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 802 | 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 803 | 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 804 | 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 805 | 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 806 | 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 807 | 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 808 | 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 809 | 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 810 | 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 811 | 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 812 | 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 813 | 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 814 | 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 815 | 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 816 | 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 817 | 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 818 | 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 819 | 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 820 | 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 821 | 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 822 | 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 823 | 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 824 | 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 825 | 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 826 | 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 827 | 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 > |