HomeHome brismu bridi
Theorem List (p. 2 of 11)
< Previous  Next >

Mirrors  >  Metamath Home Page  >  Home Page  >  Theorem List Contents       This page: Page List

Theorem List for brismu bridi - 101-200   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorembi 101 Like modus ponens ax-mp 10 but for biconditionals. (Contributed by la korvo, 16-Jul-2023.)
broda   &   ⊢ go broda gi brode   =>   ⊢ brode
 
Theorembi-rev 102 Modus ponens in the other direction. (Contributed by la korvo, 16-Jul-2023.)
broda   &   ⊢ go brode gi broda   =>   ⊢ brode
 
Theorembi-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
 
Theoremsylbi 104 Syllogism with a biconditional. (Contributed by la korvo, 25-Jun-2024.)
go broda gi brode   &   ⊢ ganai brode gi brodi   =>   ⊢ ganai broda gi brodi
 
Theoremsylib 105 Syllogism with a biconditional. (Contributed by la korvo, 25-Jun-2024.)
ganai broda gi brode   &   ⊢ go brode gi brodi   =>   ⊢ ganai broda gi brodi
 
Theoremsylibr 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
 
Theoremsylanbrc 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
 
Theoremsyl5bi 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
 
1.5  Implication II

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.

 
1.5.1  {na.a}
 
Syntaxsjnaa 109

sumti ko'a na.a ko'e
 
Definitiondf-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
 
Theoremnaai 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
 
Theoremnaaii 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
 
Theoremnaari 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
 
Theoremna.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
 
1.5.2  {.anai}
 
Syntaxsjanai 115

sumti ko'a .anai ko'e
 
Definitiondf-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
 
Theoremanaii 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
 
Theoremanaiii 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
 
Theoremanairi 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
 
1.5.3  {naja}
 
Syntaxsbnaja 120*

selbri bu'a naja bu'e
 
Definitiondf-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
 
Theoremnajai 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
 
Theoremnajaii 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
 
Theoremnajari 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
 
Definitiondf-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
 
1.5.4  {janai}
 
Syntaxsbjanai 126*

selbri bu'a janai bu'e
 
Definitiondf-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
 
Theoremjanaii 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
 
Theoremjanaiii 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
 
Theoremjanairi 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
 
1.5.5  {nagi'a}
 
Syntaxtnagiha 131

brirebla bo'a nagi'a bo'e
 
Definitiondf-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
 
Theoremnagihai 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
 
Theoremnagihaii 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
 
Theoremnagihari 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
 
1.5.6  {gi'anai}
 
Syntaxtgihanai 136

brirebla bo'a gi'anai bo'e
 
Definitiondf-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
 
Theoremgihanaii 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
 
Theoremgihanaiii 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
 
Theoremgihanairi 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
 
1.6  Conjunctions II
 
1.6.1  More facts about {ge}
 
Theoremge-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.]
 
Theoremge-com 142 {ge} is commutative. (Contributed by la korvo, 31-Jul-2023.)
go ge broda gi brode gi ge brode gi broda
 
Theoremge-go 143 Conjunction implies biimplication. (Contributed by la korvo, 25-Jun-2024.)
ge broda gi brode   =>   ⊢ go broda gi brode
 
Theoremge-diag 144 {ge} admits the diagonal morphism. (Contributed by la korvo, 21-Aug-2024.)
ganai broda gi ge broda gi broda
 
Theoremge-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
 
1.6.2  {.e}
 
Syntaxsje 146

sumti ko'a .e ko'e
 
Definitiondf-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
 
Theoremei 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
 
Theoremeri 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
 
Theoreme-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
 
1.6.3  {je}
 
Syntaxsbje 151*

selbri bu'a je bu'e
 
Definitiondf-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
 
Theoremjei 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
 
Theoremjeri 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
 
1.6.4  {gi'e}
 
Syntaxtgihe 155

brirebla bo'a gi'e bo'e
 
Definitiondf-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
 
Theoremgihei 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
 
Theoremgiheri 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
 
Theoremgiherii 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
 
1.7  Disjunctions: {ga}, {.a}, {ja}, {gi'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.

 
1.7.1  {ga}
 
Syntaxbga 160

bridi ga broda gi brode
 
Definitiondf-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
 
Theoremgai 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
 
Theoremgar 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
 
Theoremgari 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
 
Theoremga-lin 165 Introduce {ga} with the antecedent on the left. (Contributed by la korvo, 31-Jul-2023.)
ganai broda gi ga broda gi brode
 
Theoremga-rin 166 Introduce {ga} with the antecedent on the right. (Contributed by la korvo, 31-Jul-2023.)
ganai broda gi ga brode gi broda
 
Theoremga-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
 
Theoremgarid 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
 
Theoremgaridan 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
 
Theoremgarian 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
 
Theoremga-idem 171 {ga} is idempotent. (Contributed by la korvo, 15-Aug-2024.)
go ga broda gi broda gi broda
 
Theoremga-com-lem 172 Lemma for ga-com 173 (Contributed by la korvo, 31-Jul-2023.) [Auxiliary lemma - not displayed.]
 
Theoremga-com 173 {ga} commutes. (Contributed by la korvo, 31-Jul-2023.)
go ga broda gi brode gi ga brode gi broda
 
Theoremge-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
 
Theoremga-li 175 Deduce a disjunction on the left. (Contributed by la korvo, 4-Jan-2025.)
broda   =>   ⊢ ga broda gi brode
 
Theoremga-ri 176 Deduce a disjunction on the right. (Contributed by la korvo, 4-Jan-2025.)
broda   =>   ⊢ ga brode gi broda
 
Theoremga-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
 
Theoremga-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
 
Theoremga-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
 
Theoremga-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
 
Theoremga-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
 
Theoremga-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
 
1.7.2  {.a}
 
Syntaxsja 183

sumti ko'a .a ko'e
 
Definitiondf-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
 
Theoremai 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
 
Theoremari 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
 
Theorema-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
 
Theorema-comi 188 Inference form of a-com 187
ko'a .a ko'e bo'a   =>   ⊢ ko'e .a ko'a bo'a
 
1.7.3  {ja}
 
Syntaxsbja 189*

selbri bu'a ja bu'e
 
Definitiondf-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
 
Theoremjai 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
 
Theoremjari 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
 
1.7.4  {gi'a}
 
Syntaxtgiha 193

brirebla bo'a gi'a bo'e
 
Definitiondf-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
 
Theoremgihai 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
 
Theoremgihari 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
 
1.8  Biconditionals II
 
1.8.1  {.o}
 
Syntaxsjo 197

sumti ko'a .o ko'e
 
Definitiondf-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
 
Theoremoi 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
 
Theoremori 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 >

Page List
Jump to page: Contents  1 1-100101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1048
  Copyright terms: Public domain < Previous  Next >