Home | Metamath
Proof Explorer Theorem List (p. 3 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | impbid21d 201 | Deduce an equivalence from two implications. (Contributed by Wolf Lammen, 12-May-2013.) |
Theorem | impbid 202 | Deduce an equivalence from two implications. Deduction associated with impbi 198 and impbii 199. (Contributed by NM, 24-Jan-1993.) Revised to prove it from impbid21d 201. (Revised by Wolf Lammen, 3-Nov-2012.) |
Theorem | dfbi1 203 | Relate the biconditional connective to primitive connectives. See dfbi1ALT 204 for an unusual version proved directly from axioms. (Contributed by NM, 29-Dec-1992.) |
Theorem | dfbi1ALT 204 | Alternate proof of dfbi1 203. This proof, discovered by Gregory Bush on 8-Mar-2004, has several curious properties. First, it has only 17 steps directly from the axioms and df-bi 197, compared to over 800 steps were the proof of dfbi1 203 expanded into axioms. Second, step 2 demands only the property of "true"; any axiom (or theorem) could be used. It might be thought, therefore, that it is in some sense redundant, but in fact no proof is shorter than this (measured by number of steps). Third, it illustrates how intermediate steps can "blow up" in size even in short proofs. Fourth, the compressed proof is only 182 bytes (or 17 bytes in D-proof notation), but the generated web page is over 200kB with intermediate steps that are essentially incomprehensible to humans (other than Gregory Bush). If there were an obfuscated code contest for proofs, this would be a contender. This "blowing up" and incomprehensibility of the intermediate steps vividly demonstrate the advantages of using many layered intermediate theorems, since each theorem is easier to understand. (Contributed by Gregory Bush, 10-Mar-2004.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | biimp 205 | Property of the biconditional connective. (Contributed by NM, 11-May-1999.) |
Theorem | biimpi 206 | Infer an implication from a logical equivalence. Inference associated with biimp 205. (Contributed by NM, 29-Dec-1992.) |
Theorem | sylbi 207 | A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by NM, 3-Jan-1993.) |
Theorem | sylib 208 | A mixed syllogism inference from an implication and a biconditional. (Contributed by NM, 3-Jan-1993.) |
Theorem | sylbb 209 | A mixed syllogism inference from two biconditionals. (Contributed by BJ, 30-Mar-2019.) |
Theorem | biimpr 210 | Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.) |
Theorem | bicom1 211 | Commutative law for the biconditional. (Contributed by Wolf Lammen, 10-Nov-2012.) |
Theorem | bicom 212 | Commutative law for the biconditional. Theorem *4.21 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.) |
Theorem | bicomd 213 | Commute two sides of a biconditional in a deduction. (Contributed by NM, 14-May-1993.) |
Theorem | bicomi 214 | Inference from commutative law for logical equivalence. (Contributed by NM, 3-Jan-1993.) |
Theorem | impbid1 215 | Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) |
Theorem | impbid2 216 | Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) (Proof shortened by Wolf Lammen, 27-Sep-2013.) |
Theorem | impcon4bid 217 | A variation on impbid 202 with contraposition. (Contributed by Jeff Hankins, 3-Jul-2009.) |
Theorem | biimpri 218 | Infer a converse implication from a logical equivalence. Inference associated with biimpr 210. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 16-Sep-2013.) |
Theorem | biimpd 219 | Deduce an implication from a logical equivalence. Deduction associated with biimp 205 and biimpi 206. (Contributed by NM, 11-Jan-1993.) |
Theorem | mpbi 220 | An inference from a biconditional, related to modus ponens. (Contributed by NM, 11-May-1993.) |
Theorem | mpbir 221 | An inference from a biconditional, related to modus ponens. (Contributed by NM, 28-Dec-1992.) |
Theorem | mpbid 222 | A deduction from a biconditional, related to modus ponens. (Contributed by NM, 21-Jun-1993.) |
Theorem | mpbii 223 | An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 16-May-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.) |
Theorem | sylibr 224 | A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition. (Contributed by NM, 3-Jan-1993.) |
Theorem | sylbir 225 | A mixed syllogism inference from a biconditional and an implication. (Contributed by NM, 3-Jan-1993.) |
Theorem | sylbbr 226 |
A mixed syllogism inference from two biconditionals.
Note on the various syllogism-like statements in set.mm. The hypothetical syllogism syl 17 infers an implication from two implications (and there are 3syl 18 and 4syl 19 for chaining more inferences). There are four inferences inferring an implication from one implication and one biconditional: sylbi 207, sylib 208, sylbir 225, sylibr 224; four inferences inferring an implication from two biconditionals: sylbb 209, sylbbr 226, sylbb1 227, sylbb2 228; four inferences inferring a biconditional from two biconditionals: bitri 264, bitr2i 265, bitr3i 266, bitr4i 267 (and more for chaining more biconditionals). There are also closed forms and deduction versions of these, like, among many others, syld 47, syl5 34, syl6 35, mpbid 222, bitrd 268, syl5bb 272, syl6bb 276 and variants. (Contributed by BJ, 21-Apr-2019.) |
Theorem | sylbb1 227 | A mixed syllogism inference from two biconditionals. (Contributed by BJ, 21-Apr-2019.) |
Theorem | sylbb2 228 | A mixed syllogism inference from two biconditionals. (Contributed by BJ, 21-Apr-2019.) |
Theorem | sylibd 229 | A syllogism deduction. (Contributed by NM, 3-Aug-1994.) |
Theorem | sylbid 230 | A syllogism deduction. (Contributed by NM, 3-Aug-1994.) |
Theorem | mpbidi 231 | A deduction from a biconditional, related to modus ponens. (Contributed by NM, 9-Aug-1994.) |
Theorem | syl5bi 232 | A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded antecedent with a definition. (Contributed by NM, 12-Jan-1993.) |
Theorem | syl5bir 233 | A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-1993.) |
Theorem | syl5ib 234 | A mixed syllogism inference. (Contributed by NM, 12-Jan-1993.) |
Theorem | syl5ibcom 235 | A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.) |
Theorem | syl5ibr 236 | A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.) |
Theorem | syl5ibrcom 237 | A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.) |
Theorem | biimprd 238 | Deduce a converse implication from a logical equivalence. Deduction associated with biimpr 210 and biimpri 218. (Contributed by NM, 11-Jan-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.) |
Theorem | biimpcd 239 | Deduce a commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 22-Sep-2013.) |
Theorem | biimprcd 240 | Deduce a converse commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2013.) |
Theorem | syl6ib 241 | A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-1993.) |
Theorem | syl6ibr 242 | A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. (Contributed by NM, 10-Jan-1993.) |
Theorem | syl6bi 243 | A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.) |
Theorem | syl6bir 244 | A mixed syllogism inference. (Contributed by NM, 18-May-1994.) |
Theorem | syl7bi 245 | A mixed syllogism inference from a doubly nested implication and a biconditional. (Contributed by NM, 14-May-1993.) |
Theorem | syl8ib 246 | A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 1-Aug-1994.) |
Theorem | mpbird 247 | A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.) |
Theorem | mpbiri 248 | An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.) |
Theorem | sylibrd 249 | A syllogism deduction. (Contributed by NM, 3-Aug-1994.) |
Theorem | sylbird 250 | A syllogism deduction. (Contributed by NM, 3-Aug-1994.) |
Theorem | biid 251 | Principle of identity for logical equivalence. Theorem *4.2 of [WhiteheadRussell] p. 117. This is part of Frege's eighth axiom per Proposition 54 of [Frege1879] p. 50; see also eqid 2622. (Contributed by NM, 2-Jun-1993.) |
Theorem | biidd 252 | Principle of identity with antecedent. (Contributed by NM, 25-Nov-1995.) |
Theorem | pm5.1im 253 | Two propositions are equivalent if they are both true. Closed form of 2th 254. Equivalent to a biimp 205-like version of the xor-connective. This theorem stays true, no matter how you permute its operands. This is evident from its sharper version . (Contributed by Wolf Lammen, 12-May-2013.) |
Theorem | 2th 254 | Two truths are equivalent. (Contributed by NM, 18-Aug-1993.) |
Theorem | 2thd 255 | Two truths are equivalent (deduction rule). (Contributed by NM, 3-Jun-2012.) |
Theorem | ibi 256 | Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 17-Oct-2003.) |
Theorem | ibir 257 | Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 22-Jul-2004.) |
Theorem | ibd 258 | Deduction that converts a biconditional implied by one of its arguments, into an implication. Deduction associated with ibi 256. (Contributed by NM, 26-Jun-2004.) |
Theorem | pm5.74 259 | Distribution of implication over biconditional. Theorem *5.74 of [WhiteheadRussell] p. 126. (Contributed by NM, 1-Aug-1994.) (Proof shortened by Wolf Lammen, 11-Apr-2013.) |
Theorem | pm5.74i 260 | Distribution of implication over biconditional (inference rule). (Contributed by NM, 1-Aug-1994.) |
Theorem | pm5.74ri 261 | Distribution of implication over biconditional (reverse inference rule). (Contributed by NM, 1-Aug-1994.) |
Theorem | pm5.74d 262 | Distribution of implication over biconditional (deduction rule). (Contributed by NM, 21-Mar-1996.) |
Theorem | pm5.74rd 263 | Distribution of implication over biconditional (deduction rule). (Contributed by NM, 19-Mar-1997.) |
Theorem | bitri 264 | An inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.) |
Theorem | bitr2i 265 | An inference from transitive law for logical equivalence. (Contributed by NM, 12-Mar-1993.) |
Theorem | bitr3i 266 | An inference from transitive law for logical equivalence. (Contributed by NM, 2-Jun-1993.) |
Theorem | bitr4i 267 | An inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993.) |
Theorem | bitrd 268 | Deduction form of bitri 264. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 14-Apr-2013.) |
Theorem | bitr2d 269 | Deduction form of bitr2i 265. (Contributed by NM, 9-Jun-2004.) |
Theorem | bitr3d 270 | Deduction form of bitr3i 266. (Contributed by NM, 14-May-1993.) |
Theorem | bitr4d 271 | Deduction form of bitr4i 267. (Contributed by NM, 30-Jun-1993.) |
Theorem | syl5bb 272 | A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.) |
Theorem | syl5rbb 273 | A syllogism inference from two biconditionals. (Contributed by NM, 1-Aug-1993.) |
Theorem | syl5bbr 274 | A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
Theorem | syl5rbbr 275 | A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.) |
Theorem | syl6bb 276 | A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.) |
Theorem | syl6rbb 277 | A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
Theorem | syl6bbr 278 | A syllogism inference from two biconditionals. (Contributed by NM, 12-Mar-1993.) |
Theorem | syl6rbbr 279 | A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.) |
Theorem | 3imtr3i 280 | A mixed syllogism inference, useful for removing a definition from both sides of an implication. (Contributed by NM, 10-Aug-1994.) |
Theorem | 3imtr4i 281 | A mixed syllogism inference, useful for applying a definition to both sides of an implication. (Contributed by NM, 3-Jan-1993.) |
Theorem | 3imtr3d 282 | More general version of 3imtr3i 280. Useful for converting conditional definitions in a formula. (Contributed by NM, 8-Apr-1996.) |
Theorem | 3imtr4d 283 | More general version of 3imtr4i 281. Useful for converting conditional definitions in a formula. (Contributed by NM, 26-Oct-1995.) |
Theorem | 3imtr3g 284 | More general version of 3imtr3i 280. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.) |
Theorem | 3imtr4g 285 | More general version of 3imtr4i 281. Useful for converting definitions in a formula. (Contributed by NM, 20-May-1996.) (Proof shortened by Wolf Lammen, 20-Dec-2013.) |
Theorem | 3bitri 286 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993.) |
Theorem | 3bitrri 287 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.) |
Theorem | 3bitr2i 288 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.) |
Theorem | 3bitr2ri 289 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.) |
Theorem | 3bitr3i 290 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.) |
Theorem | 3bitr3ri 291 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 21-Jun-1993.) |
Theorem | 3bitr4i 292 | A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) |
Theorem | 3bitr4ri 293 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.) |
Theorem | 3bitrd 294 | Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.) |
Theorem | 3bitrrd 295 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
Theorem | 3bitr2d 296 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
Theorem | 3bitr2rd 297 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
Theorem | 3bitr3d 298 | Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.) |
Theorem | 3bitr3rd 299 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
Theorem | 3bitr4d 300 | Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 18-Oct-1995.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |