HomeTheorem List (p. 2 of 11)
Mirrors > Metamath Home Page > Home Page > Theorem List Contents This page: Page List
| Home |
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  ⊢ go
broda gi brode  ⊢ brode | ||
| Theorem | bi-rev 102 | Modus ponens in the other direction. (Contributed by la korvo, 16-Jul-2023.) |
| ⊢ broda ⊢ go
brode gi broda ⊢ brode | ||
| 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 ⊢ ganai
brode gi broda | ||
| Theorem | sylbi 104 | Syllogism with a biconditional. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ go broda gi brode ⊢ ganai
brode gi brodi ⊢ ganai
broda gi brodi | ||
| Theorem | sylib 105 | Syllogism with a biconditional. (Contributed by la korvo, 25-Jun-2024.) |
| ⊢ ganai broda gi brode ⊢ go
brode gi brodi ⊢ ganai
broda gi brodi | ||
| Theorem | sylibr 106 | Apply a definition to a consequent. (Contributed by la korvo, 22-Jun-2024.) |
| ⊢ ganai broda gi brode ⊢ go
brodi gi brode ⊢ ganai
broda gi brodi | ||
| Theorem | sylanbrc 107 | Deductive unpacking of a definition with conjoined components. (Contributed by la korvo, 22-Jun-2024.) |
| ⊢ ganai broda gi brode ⊢ ganai
broda gi brodi ⊢ go
brodo gi ge brode gi brodi ⊢ ganai
broda gi brodo | ||
| Theorem | syl5bi 108 | Replace a nested antecedent using a biconditional. (Contributed by la korvo, 22-Jun-2024.) |
| ⊢ go broda gi brode ⊢ ganai
brodi gi ganai brode gi brodo ⊢ ganai
brodi gi ganai broda gi brodo | ||
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 ⊢
ganai ko'a bo'a gi 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 ⊢ ko'a bo'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 ⊢ ko'a na.a 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 ⊢
ganai ko'a bo'a gi ko'e
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 ⊢ ko'a bo'a ⊢ ko'e 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 ⊢ ko'e .anai ko'a
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 ⊢ ganai
ko'a bu'a ko'e gi ko'a
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 ⊢ ko'a bu'a ko'e ⊢ ko'a 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 ⊢ ko'a bu'a naja
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 ⊢ ganai
ko'a bu'a ko'e gi ko'a
bu'e 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 ⊢ ko'a bu'a ko'e ⊢ ko'a bu'e 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 ⊢ ko'a bu'e
janai bu'a 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 ⊢ ganai ko'a bo'a gi
ko'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 ⊢ ko'a bo'a ⊢ ko'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 ⊢ ko'a bo'a
nagi'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 ⊢ ganai
ko'a bo'a
gi ko'a bo'e | ||
| Theorem | gihanaiii 139 | Inference form of df-gihanai 137 (Contributed by la korvo, 16-Aug-2023.) |
| ⊢ ko'a bo'e
gi'anai bo'a ⊢ ko'a bo'a ⊢ ko'a bo'e | ||
| 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 ⊢ ko'a bo'a
gi'anai bo'e | ||
| 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 ⊢ go
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 ⊢
ge ko'a bo'a gi 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 ⊢ ko'a .e 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 ⊢ ge
ko'a bu'a ko'e gi ko'a
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 ⊢ ko'a bu'a je
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 ⊢ ge ko'a bo'a gi
ko'a 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 ⊢ ko'a bo'a
gi'e bo'e | ||
| Theorem | giherii 159 | Inference form of df-gihe 156 (Contributed by la korvo, 14-Aug-2023.) |
| ⊢ ko'a bo'a ⊢ ko'a bo'e ⊢ ko'a bo'a
gi'e bo'e | ||
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 ⊢ ge
ganai brode gi broda gi ganai 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 ⊢ ganai
ga brode gi 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 ⊢ ganai
brodi gi brode ⊢ ganai
ga broda gi brodi 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 ⊢ ganai
broda gi ganai brodo gi brodi ⊢ ganai
broda gi ganai
ga brode gi brodo 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 ⊢ ganai
ge broda gi brodo gi brodi ⊢ ganai
ge broda gi
ga brode gi brodo 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 ⊢ ganai
ge brodo gi brode gi brodi ⊢ ganai
ge ga broda
gi brodo 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 ⊢ ga
broda gi brode | ||
| Theorem | ga-ri 176 | Deduce a disjunction on the right. (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ broda ⊢ ga
brode gi broda | ||
| Theorem | ga-lid 177 | Deduction form of ga-li 175 (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ ganai broda gi brode ⊢ ganai
broda gi ga brode gi brodi | ||
| Theorem | ga-rid 178 | Deduction form of ga-ri 176 (Contributed by la korvo, 4-Jan-2025.) |
| ⊢ ganai broda gi brode ⊢ ganai
broda gi ga brodi 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 ⊢ ganai
brodi gi brodo ⊢ ganai
ga broda gi brodi gi ga brode gi brodo | ||
| Theorem | ga-pairl 180 | ga-pair 179 with the arrow on the left. (Contributed by la korvo, 14-Jul-2025.) |
| ⊢ ganai broda gi brode ⊢ ganai
ga broda gi brodi gi ga brode gi brodi | ||
| Theorem | ga-pairr 181 | ga-pair 179 with the arrow on the right. (Contributed by la korvo, 14-Jul-2025.) |
| ⊢ ganai broda gi brode ⊢ ganai
ga brodi gi broda gi ga brodi 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 ⊢
ga ko'a bo'a gi 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 ⊢ ko'a .a 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 ⊢ ko'e .a ko'a
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 ⊢ ga
ko'a bu'a ko'e gi ko'a
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 ⊢ ko'a bu'a ja
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 ⊢ ga ko'a bo'a gi
ko'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 ⊢ ko'a bo'a
gi'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 ⊢
go ko'a bo'a gi 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 ⊢ ko'a .o ko'e
bo'a | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |