![]() |
brismu
bridi Theorem List (p. 2 of 11) |
< Previous Next >
|
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bi 101 | Like modus ponens ax-mp 10 but for biconditionals. (Contributed by la korvo, 16-Jul-2023.) |
⊢ broda ![]() ![]() | ||
Theorem | bi-rev 102 | Modus ponens in the other direction. (Contributed by la korvo, 16-Jul-2023.) |
⊢ broda ![]() ![]() | ||
Theorem | bi-rev-syl 103 | The right-hand side of a {go} may also be weakened to a {ganai}. (Contributed by la korvo, 10-Jul-2023.) |
⊢ go broda gi brode ![]() | ||
Theorem | sylbi 104 | Syllogism with a biconditional. (Contributed by la korvo, 25-Jun-2024.) |
⊢ go broda gi brode ![]() ![]() | ||
Theorem | sylib 105 | Syllogism with a biconditional. (Contributed by la korvo, 25-Jun-2024.) |
⊢ ganai broda gi brode ![]() ![]() | ||
Theorem | sylibr 106 | Apply a definition to a consequent. (Contributed by la korvo, 22-Jun-2024.) |
⊢ ganai broda gi brode ![]() ![]() | ||
Theorem | sylanbrc 107 | Deductive unpacking of a definition with conjoined components. (Contributed by la korvo, 22-Jun-2024.) |
⊢ ganai broda gi brode ![]() ![]() ![]() | ||
Theorem | syl5bi 108 | Replace a nested antecedent using a biconditional. (Contributed by la korvo, 22-Jun-2024.) |
⊢ go broda gi brode ![]() ![]() | ||
Unlike the other four connectives, {ganai} is not symmetric. As a result, Lojban's grammar admits both a left-to-right and right-to-left version of each connective for implication. | ||
Syntax | sjnaa 109 |
|
sumti ko'a na.a ko'e | ||
Definition | df-na.a 110 | Definition of {na.a} in terms of {ganai}. By analogy with forethought version of example 12.2-5 from [CLL] p. 14. |
⊢ go ko'a na.a ko'e bo'a gi ganai ko'a bo'a gi ko'e bo'a | ||
Theorem | naai 111 | Inference form of df-na.a 110 (Contributed by la korvo, 17-Aug-2023.) |
⊢ ko'a na.a ko'e
bo'a ![]() | ||
Theorem | naaii 112 | Inference form of df-na.a 110 (Contributed by la korvo, 17-Aug-2023.) |
⊢ ko'a na.a ko'e
bo'a ![]() ![]() | ||
Theorem | naari 113 | Reverse inference form of df-na.a 110 (Contributed by la korvo, 17-Aug-2023.) |
⊢ ganai ko'a bo'a gi
ko'e bo'a ![]() | ||
Theorem | na.a-refl 114 | {na.a} is reflexive over any brirebla. (Contributed by la korvo, 14-Aug-2024.) |
⊢ ko'a na.a ko'a bo'a | ||
Syntax | sjanai 115 |
|
sumti ko'a .anai ko'e | ||
Definition | df-anai 116 | Definition of {.anai} in terms of {ganai}. By analogy with forethought version of example 12.2-5 from [CLL] p. 14. |
⊢ go ko'e .anai ko'a bo'a gi ganai ko'a bo'a gi ko'e bo'a | ||
Theorem | anaii 117 | Inference form of df-anai 116 (Contributed by la korvo, 16-Aug-2023.) |
⊢ ko'e .anai ko'a
bo'a ![]() | ||
Theorem | anaiii 118 | Inference form of df-anai 116 (Contributed by la korvo, 16-Aug-2023.) |
⊢ ko'e .anai ko'a
bo'a ![]() ![]() | ||
Theorem | anairi 119 | Reverse inference form of df-anai 116 (Contributed by la korvo, 16-Aug-2023.) |
⊢ ganai ko'a bo'a gi
ko'e bo'a ![]() | ||
Syntax | sbnaja 120* |
|
selbri bu'a naja bu'e | ||
Definition | df-naja 121* | Definition of {naja} in terms of {ganai}. By analogy with example 12.2-5 of [CLL] p. 14. |
⊢ go ko'a bu'a naja bu'e ko'e gi ganai ko'a bu'a ko'e gi ko'a bu'e ko'e | ||
Theorem | najai 122* | Inference form of df-naja 121 (Contributed by la korvo, 17-Aug-2023.) |
⊢ ko'a bu'a naja
bu'e ko'e ![]() | ||
Theorem | najaii 123* | Inference form of df-naja 121 (Contributed by la korvo, 17-Aug-2023.) |
⊢ ko'a bu'a naja
bu'e ko'e ![]() ![]() | ||
Theorem | najari 124* | Reverse inference form of df-naja 121 (Contributed by la korvo, 17-Aug-2023.) |
⊢ ganai ko'a bu'a ko'e gi ko'a
bu'e ko'e ![]() | ||
Definition | df-naja-t 125* | Extension of df-naja 121 to ternary bridi. |
⊢ go ko'a bu'a naja bu'e ko'e ko'i gi ganai ko'a bu'a ko'e ko'i gi ko'a bu'e ko'e ko'i | ||
Syntax | sbjanai 126* |
|
selbri bu'a janai bu'e | ||
Definition | df-janai 127* | Definition of {janai} in terms of {ganai}. By analogy with example 12.2-5 of [CLL] p. 14. |
⊢ go ko'a bu'e janai bu'a ko'e gi ganai ko'a bu'a ko'e gi ko'a bu'e ko'e | ||
Theorem | janaii 128* | Inference form of df-janai 127 (Contributed by la korvo, 16-Aug-2023.) |
⊢ ko'a bu'e
janai bu'a ko'e ![]() | ||
Theorem | janaiii 129* | Inference form of df-janai 127 (Contributed by la korvo, 16-Aug-2023.) |
⊢ ko'a bu'e
janai bu'a ko'e ![]() ![]() | ||
Theorem | janairi 130* | Reverse inference form of df-janai 127 (Contributed by la korvo, 16-Aug-2023.) |
⊢ ganai ko'a bu'a ko'e gi ko'a
bu'e ko'e ![]() | ||
Syntax | tnagiha 131 |
|
brirebla bo'a nagi'a bo'e | ||
Definition | df-nagiha 132 | Definition of {nagi'a} in terms of {ganai}. |
⊢ go ko'a bo'a nagi'a bo'e gi ganai ko'a bo'a gi ko'a bo'e | ||
Theorem | nagihai 133 | Inference form of df-nagiha 132 (Contributed by la korvo, 17-Aug-2023.) |
⊢ ko'a bo'a
nagi'a bo'e ![]() | ||
Theorem | nagihaii 134 | Inference form of df-nagiha 132 (Contributed by la korvo, 17-Aug-2023.) |
⊢ ko'a bo'a
nagi'a bo'e ![]() ![]() | ||
Theorem | nagihari 135 | Inference form of df-nagiha 132 (Contributed by la korvo, 17-Aug-2023.) |
⊢ ganai ko'a bo'a gi
ko'a bo'e ![]() | ||
Syntax | tgihanai 136 |
|
brirebla bo'a gi'anai bo'e | ||
Definition | df-gihanai 137 | Definition of {gi'anai} in terms of {ganai}. |
⊢ go ko'a bo'e gi'anai bo'a gi ganai ko'a bo'a gi ko'a bo'e | ||
Theorem | gihanaii 138 | Inference form of df-gihanai 137 (Contributed by la korvo, 16-Aug-2023.) |
⊢ ko'a bo'e
gi'anai bo'a ![]() | ||
Theorem | gihanaiii 139 | Inference form of df-gihanai 137 (Contributed by la korvo, 16-Aug-2023.) |
⊢ ko'a bo'e
gi'anai bo'a ![]() ![]() | ||
Theorem | gihanairi 140 | Inference form of df-gihanai 137 (Contributed by la korvo, 16-Aug-2023.) |
⊢ ganai ko'a bo'e gi
ko'a bo'a ![]() | ||
Theorem | ge-com-lem 141 | Lemma for ge-com 142 showing that {ge} is commutative in one direction. (Contributed by la korvo, 31-Jul-2023.) [Auxiliary lemma - not displayed.] |
Theorem | ge-com 142 | {ge} is commutative. (Contributed by la korvo, 31-Jul-2023.) |
⊢ go ge broda gi brode gi ge brode gi broda | ||
Theorem | ge-go 143 | Conjunction implies biimplication. (Contributed by la korvo, 25-Jun-2024.) |
⊢ ge broda gi brode ![]() | ||
Theorem | ge-diag 144 | {ge} admits the diagonal morphism. (Contributed by la korvo, 21-Aug-2024.) |
⊢ ganai broda gi ge broda gi broda | ||
Theorem | ge-idem 145 | {ge} is idempotent. (Contributed by la korvo, 15-Aug-2024.) (Strengthened by la korvo, 21-Aug-2024.) |
⊢ go ge broda gi broda gi broda | ||
Syntax | sje 146 |
|
sumti ko'a .e ko'e | ||
Definition | df-e 147 | Definition of {.e} in terms of {ge}. Forethought version of example 12.2-5 from [CLL] p. 14. |
⊢ go ko'a .e ko'e bo'a gi ge ko'a bo'a gi ko'e bo'a | ||
Theorem | ei 148 | Inference form of df-e 147 (Contributed by la korvo, 17-Jul-2023.) |
⊢ ko'a .e ko'e
bo'a ![]() | ||
Theorem | eri 149 | Reverse inference form of df-e 147 (Contributed by la korvo, 17-Jul-2023.) |
⊢ ge ko'a bo'a gi
ko'e bo'a ![]() | ||
Theorem | e-com 150 | {.e} is commutative. (Contributed by la korvo, 21-Jul-2025.) |
⊢ go ko'a .e ko'e bo'a gi ko'e .e ko'a bo'a | ||
Syntax | sbje 151* |
|
selbri bu'a je bu'e | ||
Definition | df-je 152* | Definition of {je} in terms of {ge}. From example 12.2-5 of [CLL] p. 14. |
⊢ go ko'a bu'a je bu'e ko'e gi ge ko'a bu'a ko'e gi ko'a bu'e ko'e | ||
Theorem | jei 153* | Inference form of df-je 152 (Contributed by la korvo, 17-Jul-2023.) |
⊢ ko'a bu'a je
bu'e ko'e ![]() | ||
Theorem | jeri 154* | Reverse inference form of df-je 152 (Contributed by la korvo, 17-Jul-2023.) |
⊢ ge ko'a bu'a ko'e gi ko'a
bu'e ko'e ![]() | ||
Syntax | tgihe 155 |
|
brirebla bo'a gi'e bo'e | ||
Definition | df-gihe 156 | Definition of {gi'e} in terms of {ge}. |
⊢ go ko'a bo'a gi'e bo'e gi ge ko'a bo'a gi ko'a bo'e | ||
Theorem | gihei 157 | Inference form of df-gihe 156 (Contributed by la korvo, 14-Aug-2023.) |
⊢ ko'a bo'a
gi'e bo'e ![]() | ||
Theorem | giheri 158 | Inference form of df-gihe 156 (Contributed by la korvo, 14-Aug-2023.) |
⊢ ge ko'a bo'a gi
ko'a bo'e ![]() | ||
Theorem | giherii 159 | Inference form of df-gihe 156 (Contributed by la korvo, 14-Aug-2023.) |
⊢ ko'a bo'a ![]() ![]() | ||
Disjunctions are the first connective for which we can introduce all four forms simultaneously. The {ga} form is fundamental in our syntax, since it gives the best scoping; but we define all of the other forms so that we have them available for sugar later. | ||
Syntax | bga 160 |
|
bridi ga broda gi brode | ||
Definition | df-ga 161 | Definition of {ga} in terms of {go}, {ganai}, and {ge}. |
⊢ go ganai ga brode gi brodi gi broda gi ge ganai brode gi broda gi ganai brodi gi broda | ||
Theorem | gai 162 | Inference form of df-ga 161 (Contributed by la korvo, 28-Jul-2023.) |
⊢ ganai
ga brode gi brodi gi broda ![]() | ||
Theorem | gar 163 | Reverse implication of df-ga 161 (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai ge ganai brode gi broda gi ganai brodi gi broda gi ganai ga brode gi brodi gi broda | ||
Theorem | gari 164 | Reverse inference form of df-ga 161 (Contributed by la korvo, 28-Jul-2023.) |
⊢ ge
ganai brode gi broda gi ganai brodi gi broda ![]() | ||
Theorem | ga-lin 165 | Introduce {ga} with the antecedent on the left. (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai broda gi ga broda gi brode | ||
Theorem | ga-rin 166 | Introduce {ga} with the antecedent on the right. (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai broda gi ga brode gi broda | ||
Theorem | ga-sum 167 | All binary coproducts exist. (Contributed by la korvo, 31-Jul-2023.) |
⊢ ganai broda gi brode ![]() ![]() | ||
Theorem | garid 168 | Nested deduction form of gar 163 (Contributed by la korvo, 14-Jul-2025.) |
⊢ ganai broda gi ganai brode gi brodi ![]() ![]() | ||
Theorem | garidan 169 | Disjunction over conjunctions in the antecedents. (Contributed by la korvo, 14-Jul-2025.) |
⊢ ganai
ge broda gi brode gi brodi ![]() ![]() | ||
Theorem | garian 170 | Disjunction over conjunctions in the antecedents. (Contributed by la korvo, 14-Jul-2025.) |
⊢ ganai
ge broda gi brode gi brodi ![]() ![]() | ||
Theorem | ga-idem 171 | {ga} is idempotent. (Contributed by la korvo, 15-Aug-2024.) |
⊢ go ga broda gi broda gi broda | ||
Theorem | ga-com-lem 172 | Lemma for ga-com 173 (Contributed by la korvo, 31-Jul-2023.) [Auxiliary lemma - not displayed.] |
Theorem | ga-com 173 | {ga} commutes. (Contributed by la korvo, 31-Jul-2023.) |
⊢ go ga broda gi brode gi ga brode gi broda | ||
Theorem | ge-dist-ga 174 | {ge} distributes over {ga}. (Contributed by la korvo, 14-Jul-2025.) |
⊢ go ge broda gi ga brode gi brodi gi ga ge broda gi brode gi ge broda gi brodi | ||
Theorem | ga-li 175 | Deduce a disjunction on the left. (Contributed by la korvo, 4-Jan-2025.) |
⊢ broda ![]() | ||
Theorem | ga-ri 176 | Deduce a disjunction on the right. (Contributed by la korvo, 4-Jan-2025.) |
⊢ broda ![]() | ||
Theorem | ga-lid 177 | Deduction form of ga-li 175 (Contributed by la korvo, 4-Jan-2025.) |
⊢ ganai broda gi brode ![]() | ||
Theorem | ga-rid 178 | Deduction form of ga-ri 176 (Contributed by la korvo, 4-Jan-2025.) |
⊢ ganai broda gi brode ![]() | ||
Theorem | ga-pair 179 | A universal property of coproducts: given two arrows in Loj, there is an arrow from the coproduct of their sources to the coproduct of their targets. (Contributed by la korvo, 14-Jul-2025.) |
⊢ ganai broda gi brode ![]() ![]() | ||
Theorem | ga-pairl 180 | ga-pair 179 with the arrow on the left. (Contributed by la korvo, 14-Jul-2025.) |
⊢ ganai broda gi brode ![]() | ||
Theorem | ga-pairr 181 | ga-pair 179 with the arrow on the right. (Contributed by la korvo, 14-Jul-2025.) |
⊢ ganai broda gi brode ![]() | ||
Theorem | ga-dist-ge 182 | {ga} distributes over {ge}. (Contributed by la korvo, 14-Jul-2025.) |
⊢ go ga broda gi ge brode gi brodi gi ge ga broda gi brode gi ga broda gi brodi | ||
Syntax | sja 183 |
|
sumti ko'a .a ko'e | ||
Definition | df-a 184 | Definition of {.a} in terms of {ga}. Forethought version of example 12.2-5 from [CLL] p. 14. |
⊢ go ko'a .a ko'e bo'a gi ga ko'a bo'a gi ko'e bo'a | ||
Theorem | ai 185 | Inference form of df-a 184 (Contributed by la korvo, 14-Aug-2023.) |
⊢ ko'a .a ko'e
bo'a ![]() | ||
Theorem | ari 186 | Inference form of df-a 184 (Contributed by la korvo, 14-Aug-2023.) |
⊢ ga ko'a bo'a gi
ko'e bo'a ![]() | ||
Theorem | a-com 187 | {.a} commutes. (Contributed by la korvo, 17-Aug-2023.) |
⊢ go ko'a .a ko'e bo'a gi ko'e .a ko'a bo'a | ||
Theorem | a-comi 188 | Inference form of a-com 187 |
⊢ ko'a .a ko'e
bo'a ![]() | ||
Syntax | sbja 189* |
|
selbri bu'a ja bu'e | ||
Definition | df-ja 190* | Definition of {ja} in terms of {ga}. From example 12.2-5 of [CLL] p. 14. |
⊢ go ko'a bu'a ja bu'e ko'e gi ga ko'a bu'a ko'e gi ko'a bu'e ko'e | ||
Theorem | jai 191* | Inference form of df-ja 190 (Contributed by la korvo, 16-Aug-2023.) |
⊢ ko'a bu'a ja
bu'e ko'e ![]() | ||
Theorem | jari 192* | Reverse inference form of df-ja 190 (Contributed by la korvo, 16-Aug-2023.) |
⊢ ga ko'a bu'a ko'e gi ko'a
bu'e ko'e ![]() | ||
Syntax | tgiha 193 |
|
brirebla bo'a gi'a bo'e | ||
Definition | df-giha 194 | Definition of {gi'a} in terms of {ga}. |
⊢ go ko'a bo'a gi'a bo'e gi ga ko'a bo'a gi ko'a bo'e | ||
Theorem | gihai 195 | Inference form of df-giha 194 (Contributed by la korvo, 14-Aug-2023.) |
⊢ ko'a bo'a
gi'a bo'e ![]() | ||
Theorem | gihari 196 | Inference form of df-giha 194 (Contributed by la korvo, 14-Aug-2023.) |
⊢ ga ko'a bo'a gi
ko'a bo'e ![]() | ||
Syntax | sjo 197 |
|
sumti ko'a .o ko'e | ||
Definition | df-o 198 | Definition of {.o} in terms of {go}. By analogy with forethought version of example 12.2-5 from [CLL] p. 14. |
⊢ go ko'a .o ko'e bo'a gi go ko'a bo'a gi ko'e bo'a | ||
Theorem | oi 199 | Inference form of df-o 198 (Contributed by la korvo, 9-Aug-2023.) |
⊢ ko'a .o ko'e
bo'a ![]() | ||
Theorem | ori 200 | Reverse inference form of df-o 198 (Contributed by la korvo, 9-Aug-2023.) |
⊢ go ko'a bo'a gi
ko'e bo'a ![]() |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |