Home | Metamath
Proof Explorer Theorem List (p. 2 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 | com15 101 | Commutation of antecedents. Swap 1st and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.) (Proof shortened by Wolf Lammen, 29-Jul-2012.) |
Theorem | com52l 102 | Commutation of antecedents. Rotate left twice. (Contributed by Jeff Hankins, 28-Jun-2009.) |
Theorem | com52r 103 | Commutation of antecedents. Rotate right twice. (Contributed by Jeff Hankins, 28-Jun-2009.) |
Theorem | com5r 104 | Commutation of antecedents. Rotate right. (Contributed by Wolf Lammen, 29-Jul-2012.) |
Theorem | imim12 105 | Closed form of imim12i 62 and of 3syl 18. (Contributed by BJ, 16-Jul-2019.) |
Theorem | jarr 106 | Elimination of a nested antecedent as a partial converse of ja 173 (the other being jarl 175). (Contributed by Wolf Lammen, 9-May-2013.) |
Theorem | pm2.86d 107 | Deduction associated with pm2.86 108. (Contributed by NM, 29-Jun-1995.) (Proof shortened by Wolf Lammen, 3-Apr-2013.) |
Theorem | pm2.86 108 | Converse of axiom ax-2 7. Theorem *2.86 of [WhiteheadRussell] p. 108. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 3-Apr-2013.) |
Theorem | pm2.86i 109 | Inference associated with pm2.86 108. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Apr-2013.) |
Theorem | loolin 110 | The Linearity Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. See loowoz 111 for an alternate axiom. (Contributed by Mel L. O'Cat, 12-Aug-2004.) |
Theorem | loowoz 111 | An alternate for the Linearity Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz loolin 110, due to Barbara Wozniakowska, Reports on Mathematical Logic 10, 129-137 (1978). (Contributed by Mel L. O'Cat, 8-Aug-2004.) |
This section makes our first use of the third axiom of propositional calculus, ax-3 8. | ||
Theorem | con4 112 | Alias for ax-3 8 to be used instead of it for labeling consistency. Its associated inference is con4i 113 and its associated deduction is con4d 114. (Contributed by BJ, 24-Dec-2020.) |
Theorem | con4i 113 |
Inference associated with con4 112. Its associated inference is mt4 115.
Remark: this can also be proved using notnot 136 followed by nsyl2 142, giving a shorter proof but depending on more axioms (namely, ax-1 6 and ax-2 7). (Contributed by NM, 29-Dec-1992.) |
Theorem | con4d 114 | Deduction associated with con4 112. (Contributed by NM, 26-Mar-1995.) |
Theorem | mt4 115 | The rule of modus tollens. Inference associated with con4i 113. (Contributed by Wolf Lammen, 12-May-2013.) |
Theorem | pm2.21i 116 | A contradiction implies anything. Inference associated with pm2.21 120. Its associated inference is pm2.24ii 117. (Contributed by NM, 16-Sep-1993.) |
Theorem | pm2.24ii 117 | A contradiction implies anything. Inference associated with pm2.21i 116 and pm2.24i 146. (Contributed by NM, 27-Feb-2008.) |
Theorem | pm2.21d 118 | A contradiction implies anything. Deduction associated with pm2.21 120. (Contributed by NM, 10-Feb-1996.) |
Theorem | pm2.21ddALT 119 | Alternate proof of pm2.21dd 186. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | pm2.21 120 | From a wff and its negation, anything is true. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law. Its associated inference is pm2.21i 116. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 14-Sep-2012.) |
Theorem | pm2.24 121 | Theorem *2.24 of [WhiteheadRussell] p. 104. Its associated inference is pm2.24i 146. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.18 122 | Proof by contradiction. Theorem *2.18 of [WhiteheadRussell] p. 103. Also called the Law of Clavius. See also pm2.01 180. (Contributed by NM, 29-Dec-1992.) |
Theorem | pm2.18i 123 | Inference associated with pm2.18 122. (Contributed by BJ, 30-Mar-2020.) |
Theorem | pm2.18d 124 | Deduction based on reductio ad absurdum. (Contributed by FL, 12-Jul-2009.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Theorem | notnotr 125 | Double negation elimination. Converse of notnot 136 and one implication of notnotb 304. Theorem *2.14 of [WhiteheadRussell] p. 102. This was the fifth axiom of Frege, specifically Proposition 31 of [Frege1879] p. 44. In classical logic (our logic) this is always true. In intuitionistic logic this is not always true, and formulas for which it is true are called "stable." (Contributed by NM, 29-Dec-1992.) (Proof shortened by David Harvey, 5-Sep-1999.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |
Theorem | notnotri 126 |
Inference associated with notnotr 125.
Remark: the proof via notnotr 125 and ax-mp 5 also has three essential steps, but has a total number of steps equal to 8, instead of the present 7, because it has to construct the formula twice and the formula , whereas the present proof has to construct the formula twice and the formula , and therefore makes only one use of wn 3 instead of two. This can be checked by running the Metamath command "SHOW PROOF notnotri / NORMAL". (Contributed by NM, 27-Feb-2008.) (Proof shortened by Wolf Lammen, 15-Jul-2021.) |
Theorem | notnotriOLD 127 | Obsolete proof of notnotri 126 as of 15-Jul-2021 . (Contributed by NM, 27-Feb-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | notnotrd 128 | Deduction associated with notnotr 125 and notnotri 126. Double negation elimination rule. A translation of the natural deduction rule C , ; see natded 27260. This is Definition NNC in [Pfenning] p. 17. This rule is valid in classical logic (our logic), but not in intuitionistic logic. (Contributed by DAW, 8-Feb-2017.) |
Theorem | con2d 129 | A contraposition deduction. (Contributed by NM, 19-Aug-1993.) |
Theorem | con2 130 | Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 12-Feb-2013.) |
Theorem | mt2d 131 | Modus tollens deduction. (Contributed by NM, 4-Jul-1994.) |
Theorem | mt2i 132 | Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.) |
Theorem | nsyl3 133 | A negated syllogism inference. (Contributed by NM, 1-Dec-1995.) |
Theorem | con2i 134 | A contraposition inference. Its associated inference is mt2 191. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 13-Jun-2013.) |
Theorem | nsyl 135 | A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.) |
Theorem | notnot 136 | Double negation introduction. Converse of notnotr 125 and one implication of notnotb 304. Theorem *2.12 of [WhiteheadRussell] p. 101. This was the sixth axiom of Frege, specifically Proposition 41 of [Frege1879] p. 47. (Contributed by NM, 28-Dec-1992.) (Proof shortened by Wolf Lammen, 2-Mar-2013.) |
Theorem | notnoti 137 | Inference associated with notnot 136. (Contributed by NM, 27-Feb-2008.) |
Theorem | notnotd 138 | Deduction associated with notnot 136 and notnoti 137. (Contributed by Jarvin Udandy, 2-Sep-2016.) Avoid biconditional. (Revised by Wolf Lammen, 27-Mar-2021.) |
Theorem | con1d 139 | A contraposition deduction. (Contributed by NM, 27-Dec-1992.) |
Theorem | mt3d 140 | Modus tollens deduction. (Contributed by NM, 26-Mar-1995.) |
Theorem | mt3i 141 | Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.) |
Theorem | nsyl2 142 | A negated syllogism inference. (Contributed by NM, 26-Jun-1994.) |
Theorem | con1 143 | Contraposition. Theorem *2.15 of [WhiteheadRussell] p. 102. Its associated inference is con1i 144. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 12-Feb-2013.) |
Theorem | con1i 144 | A contraposition inference. Inference associated with con1 143. Its associated inference is mt3 192. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 19-Jun-2013.) |
Theorem | con4iOLD 145 | Obsolete proof of con4i 113 as of 15-Jul-2021. This shorter proof has been reverted to its original to avoid a dependency on ax-1 6 and ax-2 7. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 21-Jun-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | pm2.24i 146 | Inference associated with pm2.24 121. Its associated inference is pm2.24ii 117. (Contributed by NM, 20-Aug-2001.) |
Theorem | pm2.24d 147 | Deduction form of pm2.24 121. (Contributed by NM, 30-Jan-2006.) |
Theorem | con3d 148 | A contraposition deduction. Deduction form of con3 149. (Contributed by NM, 10-Jan-1993.) |
Theorem | con3 149 | Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. This was the fourth axiom of Frege, specifically Proposition 28 of [Frege1879] p. 43. Its associated inference is con3i 150. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 13-Feb-2013.) |
Theorem | con3i 150 | A contraposition inference. Inference associated with con3 149. Its associated inference is mto 188. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.) |
Theorem | con3rr3 151 | Rotate through consequent right. (Contributed by Wolf Lammen, 3-Nov-2013.) |
Theorem | mt4d 152 | Modus tollens deduction. Deduction form of mt4 115. (Contributed by NM, 9-Jun-2006.) |
Theorem | mt4i 153 | Modus tollens inference. (Contributed by Wolf Lammen, 12-May-2013.) |
Theorem | nsyld 154 | A negated syllogism deduction. (Contributed by NM, 9-Apr-2005.) |
Theorem | nsyli 155 | A negated syllogism inference. (Contributed by NM, 3-May-1994.) |
Theorem | nsyl4 156 | A negated syllogism inference. (Contributed by NM, 15-Feb-1996.) |
Theorem | pm3.2im 157 | Theorem *3.2 of [WhiteheadRussell] p. 111, expressed with primitive connectives (see pm3.2 463). (Contributed by NM, 29-Dec-1992.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |
Theorem | mth8 158 | Theorem 8 of [Margaris] p. 60. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |
Theorem | jc 159 | Deduction joining the consequents of two premises. A deduction associated with pm3.2im 157. (Contributed by NM, 28-Dec-1992.) |
Theorem | impi 160 | An importation inference. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 20-Jul-2013.) |
Theorem | expi 161 | An exportation inference. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) |
Theorem | simprim 162 | Simplification. Similar to Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.) |
Theorem | simplim 163 | Simplification. Similar to Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 21-Jul-2012.) |
Theorem | pm2.5 164 | Theorem *2.5 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 9-Oct-2012.) |
Theorem | pm2.51 165 | Theorem *2.51 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.521 166 | Theorem *2.521 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 8-Oct-2012.) |
Theorem | pm2.52 167 | Theorem *2.52 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 8-Oct-2012.) |
Theorem | expt 168 | Exportation theorem ex 450 expressed with primitive connectives. (Contributed by NM, 28-Dec-1992.) |
Theorem | impt 169 | Importation theorem imp 445 expressed with primitive connectives. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jul-2013.) |
Theorem | pm2.61d 170 | Deduction eliminating an antecedent. (Contributed by NM, 27-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.) |
Theorem | pm2.61d1 171 | Inference eliminating an antecedent. (Contributed by NM, 15-Jul-2005.) |
Theorem | pm2.61d2 172 | Inference eliminating an antecedent. (Contributed by NM, 18-Aug-1993.) |
Theorem | ja 173 | Inference joining the antecedents of two premises. For partial converses, see jarr 106 and jarl 175. (Contributed by NM, 24-Jan-1993.) (Proof shortened by Mel L. O'Cat, 19-Feb-2008.) |
Theorem | jad 174 | Deduction form of ja 173. (Contributed by Scott Fenton, 13-Dec-2010.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
Theorem | jarl 175 | Elimination of a nested antecedent as a partial converse of ja 173 (the other being jarr 106). (Contributed by Wolf Lammen, 10-May-2013.) |
Theorem | pm2.61i 176 | Inference eliminating an antecedent. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.) |
Theorem | pm2.61ii 177 | Inference eliminating two antecedents. (Contributed by NM, 4-Jan-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |
Theorem | pm2.61nii 178 | Inference eliminating two antecedents. (Contributed by NM, 13-Jul-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 13-Nov-2012.) |
Theorem | pm2.61iii 179 | Inference eliminating three antecedents. (Contributed by NM, 2-Jan-2002.) (Proof shortened by Wolf Lammen, 22-Sep-2013.) |
Theorem | pm2.01 180 | Reductio ad absurdum. Theorem *2.01 of [WhiteheadRussell] p. 100. Also called the weak Clavius law, and provable in minimal calculus, contrary to the Clavius law pm2.18 122. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Mel L. O'Cat, 21-Nov-2008.) (Proof shortened by Wolf Lammen, 31-Oct-2012.) |
Theorem | pm2.01d 181 | Deduction based on reductio ad absurdum. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Mar-2013.) |
Theorem | pm2.6 182 | Theorem *2.6 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.61 183 | Theorem *2.61 of [WhiteheadRussell] p. 107. Useful for eliminating an antecedent. (Contributed by NM, 4-Jan-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.) |
Theorem | pm2.65 184 | Theorem *2.65 of [WhiteheadRussell] p. 107. Proof by contradiction. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 8-Mar-2013.) |
Theorem | pm2.65i 185 | Inference rule for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
Theorem | pm2.21dd 186 | A contradiction implies anything. Deduction from pm2.21 120. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 22-Jul-2019.) |
Theorem | pm2.65d 187 | Deduction rule for proof by contradiction. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 26-May-2013.) |
Theorem | mto 188 | 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 mode that by denying denies" - remark in [Sanford] p. 39. It is also called denying the consequent. Modus tollens is closely related to modus ponens ax-mp 5. Note that this rule is also valid in intuitionistic logic. Inference associated with con3i 150. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
Theorem | mtod 189 | Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
Theorem | mtoi 190 | Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.) |
Theorem | mt2 191 | A rule similar to modus tollens. Inference associated with con2i 134. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Sep-2013.) |
Theorem | mt3 192 | A rule similar to modus tollens. Inference associated with con1i 144. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
Theorem | peirce 193 | 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 6 through ax-3 8. A notable fact about this theorem is that it requires ax-3 8 for its proof even though the result has no negation connectives in it. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 9-Oct-2012.) |
Theorem | looinv 194 | The Inversion Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. Using dfor2 427, we can see that this essentially expresses "disjunction commutes." Theorem *2.69 of [WhiteheadRussell] p. 108. It is a special instance of the axiom "Roll", see peirceroll 85. (Contributed by NM, 12-Aug-2004.) |
Theorem | bijust 195 | Theorem used to justify definition of biconditional df-bi 197. (Contributed by NM, 11-May-1999.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |
The definition df-bi 197 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 385 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 196 | Extend our wff definition to include the biconditional connective. |
Definition | df-bi 197 |
Define the biconditional (logical 'iff').
The definition df-bi 197 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 385 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 1039) 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 195. It is impossible to use df-bi 197 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 197 in the proof with the corresponding bijust 195 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 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 1486) and the constant false (df-fal 1489), we will be able to prove these truth table values: (trubitru 1520), (trubifal 1522), (falbitru 1521), and (falbifal 1523). See dfbi1 203, dfbi2 660, and dfbi3 994 for theorems suggesting typical textbook definitions of , showing that our definition has the properties we expect. Theorem dfbi1 203 is particularly useful if we want to eliminate from an expression to convert it to primitives. Theorem dfbi 661 shows this definition rewritten in an abbreviated form after conjunction is introduced, for easier understanding. Contrast with (df-or 385), (wi 4), (df-nan 1448), and (df-xor 1465) . In some sense returns true if two truth values are equal; (df-cleq 2615) returns true if two classes are equal. (Contributed by NM, 27-Dec-1992.) |
Theorem | impbi 198 | Property of the biconditional connective. (Contributed by NM, 11-May-1999.) |
Theorem | impbii 199 | Infer an equivalence from an implication and its converse. Inference associated with impbi 198. (Contributed by NM, 29-Dec-1992.) |
Theorem | impbidd 200 | Deduce an equivalence from two implications. Double deduction associated with impbi 198 and impbii 199. Deduction associated with impbid 202. (Contributed by Rodolfo Medina, 12-Oct-2010.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |