Home | Metamath
Proof ExplorerTheorem List
(p. 2 of 315)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs

Color key: | Metamath Proof Explorer
(1-21490) |
Hilbert Space Explorer
(21491-23013) |
Users' Mathboxes
(23014-31421) |

Type | Label | Description |
---|---|---|

Statement | ||

Theorem | pm2.21dd 101 | A contradiction implies anything. Deduction from pm2.21 102. (Contributed by Mario Carneiro, 9-Feb-2017.) |

Theorem | pm2.21 102 | From a wff and its negation, anything is true. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Sep-2012.) |

Theorem | pm2.24 103 | Theorem *2.24 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |

Theorem | pm2.18 104 | Proof by contradiction. Theorem *2.18 of [WhiteheadRussell] p. 103. Also called the Law of Clavius. (Contributed by NM, 5-Aug-1993.) |

Theorem | pm2.18d 105 | Deduction based on reductio ad absurdum. (Contributed by FL, 12-Jul-2009.) (Proof shortened by Andrew Salmon, 7-May-2011.) |

Theorem | notnot2 106 | Converse of double negation. Theorem *2.14 of [WhiteheadRussell] p. 102. (Contributed by NM, 5-Aug-1993.) (Proof shortened by David Harvey, 5-Sep-1999.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |

Theorem | notnotrd 107 | Deduction converting double-negation into the original wff, aka the double negation rule. A translation of natural deduction rule -C, => ; see natded 4. This is definition NNC in [Pfenning] p. 17. This rule is valid in classical logic (which MPE uses), but not intuitionistic logic. (Contributed by DAW, 8-Feb-2017.) |

Theorem | notnotri 108 | Inference from double negation. (Contributed by NM, 27-Feb-2008.) |

Theorem | con2d 109 | A contraposition deduction. (Contributed by NM, 19-Aug-1993.) |

Theorem | con2 110 | Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Feb-2013.) |

Theorem | mt2d 111 | Modus tollens deduction. (Contributed by NM, 4-Jul-1994.) |

Theorem | mt2i 112 | Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.) |

Theorem | nsyl3 113 | A negated syllogism inference. (Contributed by NM, 1-Dec-1995.) |

Theorem | con2i 114 | A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 13-Jun-2013.) |

Theorem | nsyl 115 | A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.) |

Theorem | notnot1 116 | Converse of double negation. Theorem *2.12 of [WhiteheadRussell] p. 101. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.) |

Theorem | notnoti 117 | Infer double negation. (Contributed by NM, 27-Feb-2008.) |

Theorem | con1d 118 | A contraposition deduction. (Contributed by NM, 5-Aug-1993.) |

Theorem | mt3d 119 | Modus tollens deduction. (Contributed by NM, 26-Mar-1995.) |

Theorem | mt3i 120 | Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.) |

Theorem | nsyl2 121 | A negated syllogism inference. (Contributed by NM, 26-Jun-1994.) |

Theorem | con1 122 | Contraposition. Theorem *2.15 of [WhiteheadRussell] p. 102. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Feb-2013.) |

Theorem | con1i 123 | A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 19-Jun-2013.) |

Theorem | con4i 124 | Inference rule derived from axiom ax-3 9. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Jun-2013.) |

Theorem | pm2.21i 125 | A contradiction implies anything. Inference from pm2.21 102. (Contributed by NM, 16-Sep-1993.) |

Theorem | pm2.24ii 126 | A contradiction implies anything. Inference from pm2.24 103. (Contributed by NM, 27-Feb-2008.) |

Theorem | con3d 127 | A contraposition deduction. (Contributed by NM, 5-Aug-1993.) |

Theorem | con3 128 | Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Feb-2013.) |

Theorem | con3i 129 | A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.) |

Theorem | con3rr3 130 | Rotate through consequent right. (Contributed by Wolf Lammen, 3-Nov-2013.) |

Theorem | mt4 131 | The rule of modus tollens. (Contributed by Wolf Lammen, 12-May-2013.) |

Theorem | mt4d 132 | Modus tollens deduction. (Contributed by NM, 9-Jun-2006.) |

Theorem | mt4i 133 | Modus tollens inference. (Contributed by Wolf Lammen, 12-May-2013.) |

Theorem | nsyld 134 | A negated syllogism deduction. (Contributed by NM, 9-Apr-2005.) |

Theorem | nsyli 135 | A negated syllogism inference. (Contributed by NM, 3-May-1994.) |

Theorem | nsyl4 136 | A negated syllogism inference. (Contributed by NM, 15-Feb-1996.) |

Theorem | pm2.24d 137 | Deduction version of pm2.24 103. (Contributed by NM, 30-Jan-2006.) |

Theorem | pm2.24i 138 | Inference version of pm2.24 103. (Contributed by NM, 20-Aug-2001.) |

Theorem | pm3.2im 139 | Theorem *3.2 of [WhiteheadRussell] p. 111, expressed with primitive connectives. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |

Theorem | mth8 140 | Theorem 8 of [Margaris] p. 60. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |

Theorem | jc 141 | Inference joining the consequents of two premises. (Contributed by NM, 5-Aug-1993.) |

Theorem | impi 142 | An importation inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 20-Jul-2013.) |

Theorem | expi 143 | An exportation inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.) |

Theorem | simprim 144 | Simplification. Similar to Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.) |

Theorem | simplim 145 | Simplification. Similar to Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Jul-2012.) |

Theorem | pm2.5 146 | Theorem *2.5 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 9-Oct-2012.) |

Theorem | pm2.51 147 | Theorem *2.51 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |

Theorem | pm2.521 148 | Theorem *2.521 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 8-Oct-2012.) |

Theorem | pm2.52 149 | Theorem *2.52 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 8-Oct-2012.) |

Theorem | expt 150 | Exportation theorem expressed with primitive connectives. (Contributed by NM, 5-Aug-1993.) |

Theorem | impt 151 | Importation theorem expressed with primitive connectives. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jul-2013.) |

Theorem | pm2.61d 152 | Deduction eliminating an antecedent. (Contributed by NM, 27-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.) |

Theorem | pm2.61d1 153 | Inference eliminating an antecedent. (Contributed by NM, 15-Jul-2005.) |

Theorem | pm2.61d2 154 | Inference eliminating an antecedent. (Contributed by NM, 18-Aug-1993.) |

Theorem | ja 155 | Inference joining the antecedents of two premises. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 19-Feb-2008.) |

Theorem | jad 156 | Deduction form of ja 155. (Contributed by Scott Fenton, 13-Dec-2010.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |

Theorem | jarl 157 | Elimination of a nested antecedent as a kind of reversal of inference ja 155. (Contributed by Wolf Lammen, 10-May-2013.) |

Theorem | pm2.61i 158 | Inference eliminating an antecedent. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.) |

Theorem | pm2.61ii 159 | Inference eliminating two antecedents. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |

Theorem | pm2.61nii 160 | Inference eliminating two antecedents. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 13-Nov-2012.) |

Theorem | pm2.61iii 161 | Inference eliminating three antecedents. (Contributed by NM, 2-Jan-2002.) (Proof shortened by Wolf Lammen, 22-Sep-2013.) |

Theorem | pm2.01 162 | Reductio ad absurdum. Theorem *2.01 of [WhiteheadRussell] p. 100. (Contributed by NM, 18-Aug-1993.) (Proof shortened by O'Cat, 21-Nov-2008.) (Proof shortened by Wolf Lammen, 31-Oct-2012.) |

Theorem | pm2.01d 163 | Deduction based on reductio ad absurdum. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Mar-2013.) |

Theorem | pm2.6 164 | Theorem *2.6 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |

Theorem | pm2.61 165 | Theorem *2.61 of [WhiteheadRussell] p. 107. Useful for eliminating an antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.) |

Theorem | pm2.65 166 | Theorem *2.65 of [WhiteheadRussell] p. 107. Proof by contradiction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 8-Mar-2013.) |

Theorem | pm2.65i 167 | Inference rule for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |

Theorem | pm2.65d 168 | Deduction rule for proof by contradiction. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 26-May-2013.) |

Theorem | mto 169 | The rule of modus tollens. The rule says, "if is not true, and implies , then must also be not true." Modus tollens is short for "modus tollendo tollens," a Latin phrase that means "the mood that by denying affirms" [Sanford] p. 39. It is also called denying the consequent. Modus tollens is closely related to modus ponens ax-mp 10. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |

Theorem | mtod 170 | Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |

Theorem | mtoi 171 | Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.) |

Theorem | mt2 172 | A rule similar to modus tollens. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Sep-2013.) |

Theorem | mt3 173 | A rule similar to modus tollens. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |

Theorem | peirce 174 | Peirce's axiom. This odd-looking theorem is the "difference" between an intuitionistic system of propositional calculus and a classical system and is not accepted by intuitionists. When Peirce's axiom is added to an intuitionistic system, the system becomes equivalent to our classical system ax-1 7 through ax-3 9. A curious fact about this theorem is that it requires ax-3 9 for its proof even though the result has no negation connectives in it. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 9-Oct-2012.) |

Theorem | loolin 175 | The Linearity Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. For a version not using ax-3 9, see loolinALT 97. (Contributed by O'Cat, 12-Aug-2004.) (Proof shortened by Wolf Lammen, 2-Nov-2012.) |

Theorem | looinv 176 | The Inversion Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. Using dfor2 402, we can see that this essentially expresses "disjunction commutes." Theorem *2.69 of [WhiteheadRussell] p. 108. (Contributed by NM, 12-Aug-2004.) |

Theorem | bijust 177 | Theorem used to justify definition of biconditional df-bi 179. (Contributed by NM, 11-May-1999.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |

1.3.5 Logical equivalenceThe definition df-bi 179 in this section is our first definition, which introduces and defines the biconditional connective . We define a wff of the form as an abbreviation for . Unlike most traditional developments, we have chosen not to have a separate symbol such as "Df." to mean "is defined as." Instead, we will later use the biconditional connective for this purpose (df-or 361 is its first use), as it allows us to use logic to manipulate definitions directly. This greatly simplifies many proofs since it eliminates the need for a separate mechanism for introducing and eliminating definitions. | ||

Syntax | wb 178 | Extend our wff definition to include the biconditional connective. |

Definition | df-bi 179 |
Define the biconditional (logical 'iff').
The definition df-bi 179 in this section is our first definition, which introduces and defines the biconditional connective . We define a wff of the form as an abbreviation for . Unlike most traditional developments, we have chosen not to have a separate symbol such as "Df." to mean "is defined as." Instead, we will later use the biconditional connective for this purpose (df-or 361 is its first use), as it allows us to use logic to manipulate definitions directly. This greatly simplifies many proofs since it eliminates the need for a separate mechanism for introducing and eliminating definitions. Of course, we cannot use this mechanism to define the biconditional itself, since it hasn't been introduced yet. Instead, we use a more general form of definition, described as follows. In its most general form, a definition is simply an assertion that introduces a new symbol (or a new combination of existing symbols, as in df-3an 938) that is eliminable and does not strengthen the existing language. The latter requirement means that the set of provable statements not containing the new symbol (or new combination) should remain exactly the same after the definition is introduced. Our definition of the biconditional may look unusual compared to most definitions, but it strictly satisfies these requirements. The justification for our definition is that if we mechanically replace (the definiendum i.e. the thing being defined) with (the definiens i.e. the defining expression) in the definition, the definition becomes the previously proved theorem bijust 177. It is impossible to use df-bi 179 to prove any statement expressed in the original language that can't be proved from the original axioms, because if we simply replace each instance of df-bi 179 in the proof with the corresponding bijust 177 instance, we will end up with a proof from the original axioms. Note that from Metamath's point of view, a definition is just another axiom - i.e. an assertion we claim to be true - but from our high level point of view, we are are not strengthening the language. To indicate this fact, we prefix definition labels with "df-" instead of "ax-". (This prefixing is an informal convention that means nothing to the Metamath proof verifier; it is just a naming convention for human readability.) After we define the constant true (df-tru 1312) and the constant false (df-fal 1313), we will be able to prove these truth table values: (trubitru 1342), (trubifal 1343), (falbitru 1344), and (falbifal 1345). See dfbi1 186, dfbi2 611, and dfbi3 865 for theorems suggesting typical textbook definitions of , showing that our definition has the properties we expect. Theorem dfbi1 186 is particularly useful if we want to eliminate from an expression to convert it to primitives. Theorem dfbi 612 shows this definition rewritten in an abbreviated form after conjunction is introduced, for easier understanding. Contrast with (df-or 361), (wi 6), (df-nan 1290), and (df-xor 1298) . In some sense returns true if two truth values are equal; (df-cleq 2277) returns true if two classes are equal. (Contributed by NM, 5-Aug-1993.) |

Theorem | bi1 180 | Property of the biconditional connective. (Contributed by NM, 11-May-1999.) |

Theorem | bi3 181 | Property of the biconditional connective. (Contributed by NM, 11-May-1999.) |

Theorem | impbii 182 | Infer an equivalence from an implication and its converse. (Contributed by NM, 5-Aug-1993.) |

Theorem | impbidd 183 | Deduce an equivalence from two implications. (Contributed by Rodolfo Medina, 12-Oct-2010.) |

Theorem | impbid21d 184 | Deduce an equivalence from two implications. (Contributed by Wolf Lammen, 12-May-2013.) |

Theorem | impbid 185 | Deduce an equivalence from two implications. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen, 3-Nov-2012.) |

Theorem | dfbi1 186 | Relate the biconditional connective to primitive connectives. See dfbi1gb 187 for an unusual version proved directly from axioms. (Contributed by NM, 5-Aug-1993.) |

Theorem | dfbi1gb 187 | This proof of dfbi1 186, 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 179, compared to over 800 steps were the proof of dfbi1 186 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 | biimpi 188 | Infer an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.) |

Theorem | sylbi 189 | A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by NM, 5-Aug-1993.) |

Theorem | sylib 190 | A mixed syllogism inference from an implication and a biconditional. (Contributed by NM, 5-Aug-1993.) |

Theorem | bi2 191 | Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.) |

Theorem | bicom1 192 | Commutative law for equivalence. (Contributed by Wolf Lammen, 10-Nov-2012.) |

Theorem | bicom 193 | Commutative law for equivalence. Theorem *4.21 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.) |

Theorem | bicomd 194 | Commute two sides of a biconditional in a deduction. (Contributed by NM, 5-Aug-1993.) |

Theorem | bicomi 195 | Inference from commutative law for logical equivalence. (Contributed by NM, 5-Aug-1993.) |

Theorem | impbid1 196 | Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) |

Theorem | impbid2 197 | Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) (Proof shortened by Wolf Lammen, 27-Sep-2013.) |

Theorem | impcon4bid 198 | A variation on impbid 185 with contraposition. (Contributed by Jeff Hankins, 3-Jul-2009.) |

Theorem | biimpri 199 | Infer a converse implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Sep-2013.) |

Theorem | biimpd 200 | Deduce an implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.) |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |