Home | Metamath
Proof Explorer Theorem List (p. 2 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | com52r 101 | Commutation of antecedents. Rotate right twice. (Contributed by Jeff Hankins, 28-Jun-2009.) |
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) ⇒ ⊢ (𝜃 → (𝜏 → (𝜑 → (𝜓 → (𝜒 → 𝜂))))) | ||
Theorem | com5r 102 | Commutation of antecedents. Rotate right. (Contributed by Wolf Lammen, 29-Jul-2012.) |
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) ⇒ ⊢ (𝜏 → (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜂))))) | ||
Theorem | imim12 103 | Closed form of imim12i 60 and of 3syl 18. (Contributed by BJ, 16-Jul-2019.) |
⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜃) → ((𝜓 → 𝜒) → (𝜑 → 𝜃)))) | ||
Theorem | jarr 104 | Elimination of a nested antecedent as a partial converse of ja 172 (the other being jarl 174). (Contributed by Wolf Lammen, 9-May-2013.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒)) | ||
Theorem | pm2.86d 105 | Deduction associated with pm2.86 106. (Contributed by NM, 29-Jun-1995.) (Proof shortened by Wolf Lammen, 3-Apr-2013.) |
⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | ||
Theorem | pm2.86 106 | 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 107 | Inference associated with pm2.86 106. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Apr-2013.) |
⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | pm2.86iALT 108 | Alternate proof of pm2.86i 107 with only three essential steps. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 19-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | loolin 109 | The Linearity Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. See loowoz 110 for an alternate axiom. (Contributed by Mel L. O'Cat, 12-Aug-2004.) |
⊢ (((𝜑 → 𝜓) → (𝜓 → 𝜑)) → (𝜓 → 𝜑)) | ||
Theorem | loowoz 110 | An alternate for the Linearity Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz loolin 109, 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 111 | Alias for ax-3 8 to be used instead of it for labeling consistency. Its associated inference is con4i 112 and its associated deduction is con4d 113. (Contributed by BJ, 24-Dec-2020.) |
⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑)) | ||
Theorem | con4i 112 | Inference associated with con4 111. Its associated inference is mt4 114. (Contributed by NM, 29-Dec-1992.) |
⊢ (¬ 𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜓 → 𝜑) | ||
Theorem | con4d 113 | Deduction associated with con4 111. (Contributed by NM, 26-Mar-1995.) |
⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 → 𝜓)) | ||
Theorem | mt4 114 | The rule of modus tollens. Inference associated with con4i 112. (Contributed by Wolf Lammen, 12-May-2013.) |
⊢ 𝜑 & ⊢ (¬ 𝜓 → ¬ 𝜑) ⇒ ⊢ 𝜓 | ||
Theorem | pm2.21i 115 | A contradiction implies anything. Inference associated with pm2.21 119. Its associated inference is pm2.24ii 116. (Contributed by NM, 16-Sep-1993.) |
⊢ ¬ 𝜑 ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.24ii 116 | A contradiction implies anything. Inference associated with pm2.21i 115 and pm2.24i 145. (Contributed by NM, 27-Feb-2008.) |
⊢ 𝜑 & ⊢ ¬ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | pm2.21d 117 | A contradiction implies anything. Deduction associated with pm2.21 119. (Contributed by NM, 10-Feb-1996.) |
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | pm2.21ddALT 118 | Alternate proof of pm2.21dd 185. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | pm2.21 119 | 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 115. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 14-Sep-2012.) |
⊢ (¬ 𝜑 → (𝜑 → 𝜓)) | ||
Theorem | pm2.24 120 | Theorem *2.24 of [WhiteheadRussell] p. 104. Its associated inference is pm2.24i 145. (Contributed by NM, 3-Jan-2005.) |
⊢ (𝜑 → (¬ 𝜑 → 𝜓)) | ||
Theorem | pm2.18 121 | Proof by contradiction. Theorem *2.18 of [WhiteheadRussell] p. 103. Also called the Law of Clavius. See also pm2.01 179. (Contributed by NM, 29-Dec-1992.) |
⊢ ((¬ 𝜑 → 𝜑) → 𝜑) | ||
Theorem | pm2.18i 122 | Inference associated with pm2.18 121. (Contributed by BJ, 30-Mar-2020.) |
⊢ (¬ 𝜑 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | pm2.18d 123 | Deduction based on reductio ad absurdum. (Contributed by FL, 12-Jul-2009.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ (𝜑 → (¬ 𝜓 → 𝜓)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | notnotr 124 | Double negation elimination. Converse of notnot 135 and one implication of notnotb 303. 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 125 | Inference associated with notnotr 124. (Contributed by NM, 27-Feb-2008.) (Proof shortened by Wolf Lammen, 15-Jul-2021.) |
⊢ ¬ ¬ 𝜑 ⇒ ⊢ 𝜑 | ||
Theorem | notnotriOLD 126 | Obsolete proof of notnotri 125 as of 15-Jul-2021 . (Contributed by NM, 27-Feb-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ ¬ 𝜑 ⇒ ⊢ 𝜑 | ||
Theorem | notnotrd 127 | Deduction associated with notnotr 124 and notnotri 125. Double negation elimination rule. A translation of the natural deduction rule ¬ ¬ C , Γ⊢ ¬ ¬ 𝜓 ⇒ Γ⊢ 𝜓; see natded 26652. 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 128 | A contraposition deduction. (Contributed by NM, 19-Aug-1993.) |
⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 → ¬ 𝜓)) | ||
Theorem | con2 129 | Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 12-Feb-2013.) |
⊢ ((𝜑 → ¬ 𝜓) → (𝜓 → ¬ 𝜑)) | ||
Theorem | mt2d 130 | Modus tollens deduction. (Contributed by NM, 4-Jul-1994.) |
⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | mt2i 131 | Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.) |
⊢ 𝜒 & ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | nsyl3 132 | A negated syllogism inference. (Contributed by NM, 1-Dec-1995.) |
⊢ (𝜑 → ¬ 𝜓) & ⊢ (𝜒 → 𝜓) ⇒ ⊢ (𝜒 → ¬ 𝜑) | ||
Theorem | con2i 133 | A contraposition inference. Its associated inference is mt2 190. (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 134 | A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.) |
⊢ (𝜑 → ¬ 𝜓) & ⊢ (𝜒 → 𝜓) ⇒ ⊢ (𝜑 → ¬ 𝜒) | ||
Theorem | notnot 135 | Double negation introduction. Converse of notnotr 124 and one implication of notnotb 303. 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 136 | Inference associated with notnot 135. (Contributed by NM, 27-Feb-2008.) |
⊢ 𝜑 ⇒ ⊢ ¬ ¬ 𝜑 | ||
Theorem | notnotd 137 | Deduction associated with notnot 135 and notnoti 136. (Contributed by Jarvin Udandy, 2-Sep-2016.) Avoid biconditional. (Revised by Wolf Lammen, 27-Mar-2021.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ¬ ¬ 𝜓) | ||
Theorem | con1d 138 | A contraposition deduction. (Contributed by NM, 27-Dec-1992.) |
⊢ (𝜑 → (¬ 𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (¬ 𝜒 → 𝜓)) | ||
Theorem | mt3d 139 | Modus tollens deduction. (Contributed by NM, 26-Mar-1995.) |
⊢ (𝜑 → ¬ 𝜒) & ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | mt3i 140 | Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.) |
⊢ ¬ 𝜒 & ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | nsyl2 141 | A negated syllogism inference. (Contributed by NM, 26-Jun-1994.) |
⊢ (𝜑 → ¬ 𝜓) & ⊢ (¬ 𝜒 → 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | con1 142 | Contraposition. Theorem *2.15 of [WhiteheadRussell] p. 102. Its associated inference is con1i 143. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 12-Feb-2013.) |
⊢ ((¬ 𝜑 → 𝜓) → (¬ 𝜓 → 𝜑)) | ||
Theorem | con1i 143 | A contraposition inference. Inference associated with con1 142. Its associated inference is mt3 191. (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 144 | Obsolete proof of con4i 112 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 145 | Inference associated with pm2.24 120. Its associated inference is pm2.24ii 116. (Contributed by NM, 20-Aug-2001.) |
⊢ 𝜑 ⇒ ⊢ (¬ 𝜑 → 𝜓) | ||
Theorem | pm2.24d 146 | Deduction form of pm2.24 120. (Contributed by NM, 30-Jan-2006.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) | ||
Theorem | con3d 147 | A contraposition deduction. Deduction form of con3 148. (Contributed by NM, 10-Jan-1993.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) | ||
Theorem | con3 148 | 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 149. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 13-Feb-2013.) |
⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑)) | ||
Theorem | con3i 149 | A contraposition inference. Inference associated with con3 148. Its associated inference is mto 187. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (¬ 𝜓 → ¬ 𝜑) | ||
Theorem | con3rr3 150 | Rotate through consequent right. (Contributed by Wolf Lammen, 3-Nov-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (¬ 𝜒 → (𝜑 → ¬ 𝜓)) | ||
Theorem | mt4d 151 | Modus tollens deduction. Deduction form of mt4 114. (Contributed by NM, 9-Jun-2006.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | mt4i 152 | Modus tollens inference. (Contributed by Wolf Lammen, 12-May-2013.) |
⊢ 𝜒 & ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | nsyld 153 | A negated syllogism deduction. (Contributed by NM, 9-Apr-2005.) |
⊢ (𝜑 → (𝜓 → ¬ 𝜒)) & ⊢ (𝜑 → (𝜏 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ¬ 𝜏)) | ||
Theorem | nsyli 154 | A negated syllogism inference. (Contributed by NM, 3-May-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → ¬ 𝜒) ⇒ ⊢ (𝜑 → (𝜃 → ¬ 𝜓)) | ||
Theorem | nsyl4 155 | A negated syllogism inference. (Contributed by NM, 15-Feb-1996.) |
⊢ (𝜑 → 𝜓) & ⊢ (¬ 𝜑 → 𝜒) ⇒ ⊢ (¬ 𝜒 → 𝜓) | ||
Theorem | pm3.2im 156 | Theorem *3.2 of [WhiteheadRussell] p. 111, expressed with primitive connectives (see pm3.2 462). (Contributed by NM, 29-Dec-1992.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |
⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓))) | ||
Theorem | mth8 157 | Theorem 8 of [Margaris] p. 60. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |
⊢ (𝜑 → (¬ 𝜓 → ¬ (𝜑 → 𝜓))) | ||
Theorem | jc 158 | Deduction joining the consequents of two premises. A deduction associated with pm3.2im 156. (Contributed by NM, 28-Dec-1992.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → ¬ (𝜓 → ¬ 𝜒)) | ||
Theorem | impi 159 | An importation inference. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 20-Jul-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (¬ (𝜑 → ¬ 𝜓) → 𝜒) | ||
Theorem | expi 160 | An exportation inference. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) |
⊢ (¬ (𝜑 → ¬ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | simprim 161 | 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 162 | 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 163 | Theorem *2.5 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 9-Oct-2012.) |
⊢ (¬ (𝜑 → 𝜓) → (¬ 𝜑 → 𝜓)) | ||
Theorem | pm2.51 164 | Theorem *2.51 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (𝜑 → 𝜓) → (𝜑 → ¬ 𝜓)) | ||
Theorem | pm2.521 165 | Theorem *2.521 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 8-Oct-2012.) |
⊢ (¬ (𝜑 → 𝜓) → (𝜓 → 𝜑)) | ||
Theorem | pm2.52 166 | Theorem *2.52 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 8-Oct-2012.) |
⊢ (¬ (𝜑 → 𝜓) → (¬ 𝜑 → ¬ 𝜓)) | ||
Theorem | expt 167 | Exportation theorem expressed with primitive connectives. (Contributed by NM, 28-Dec-1992.) |
⊢ ((¬ (𝜑 → ¬ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒))) | ||
Theorem | impt 168 | Importation theorem expressed with primitive connectives. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jul-2013.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (¬ (𝜑 → ¬ 𝜓) → 𝜒)) | ||
Theorem | pm2.61d 169 | Deduction eliminating an antecedent. (Contributed by NM, 27-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | pm2.61d1 170 | Inference eliminating an antecedent. (Contributed by NM, 15-Jul-2005.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (¬ 𝜓 → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | pm2.61d2 171 | Inference eliminating an antecedent. (Contributed by NM, 18-Aug-1993.) |
⊢ (𝜑 → (¬ 𝜓 → 𝜒)) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | ja 172 | Inference joining the antecedents of two premises. For partial converses, see jarr 104 and jarl 174. (Contributed by NM, 24-Jan-1993.) (Proof shortened by Mel L. O'Cat, 19-Feb-2008.) |
⊢ (¬ 𝜑 → 𝜒) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ ((𝜑 → 𝜓) → 𝜒) | ||
Theorem | jad 173 | Deduction form of ja 172. (Contributed by Scott Fenton, 13-Dec-2010.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ (𝜑 → (¬ 𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜒 → 𝜃)) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜒) → 𝜃)) | ||
Theorem | jarl 174 | Elimination of a nested antecedent as a partial converse of ja 172 (the other being jarr 104). (Contributed by Wolf Lammen, 10-May-2013.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → (¬ 𝜑 → 𝜒)) | ||
Theorem | pm2.61i 175 | Inference eliminating an antecedent. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.) |
⊢ (𝜑 → 𝜓) & ⊢ (¬ 𝜑 → 𝜓) ⇒ ⊢ 𝜓 | ||
Theorem | pm2.61ii 176 | Inference eliminating two antecedents. (Contributed by NM, 4-Jan-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |
⊢ (¬ 𝜑 → (¬ 𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | pm2.61nii 177 | 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 178 | Inference eliminating three antecedents. (Contributed by NM, 2-Jan-2002.) (Proof shortened by Wolf Lammen, 22-Sep-2013.) |
⊢ (¬ 𝜑 → (¬ 𝜓 → (¬ 𝜒 → 𝜃))) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜓 → 𝜃) & ⊢ (𝜒 → 𝜃) ⇒ ⊢ 𝜃 | ||
Theorem | pm2.01 179 | 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 121. (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 180 | Deduction based on reductio ad absurdum. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Mar-2013.) |
⊢ (𝜑 → (𝜓 → ¬ 𝜓)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | pm2.6 181 | Theorem *2.6 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
⊢ ((¬ 𝜑 → 𝜓) → ((𝜑 → 𝜓) → 𝜓)) | ||
Theorem | pm2.61 182 | 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 183 | 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 184 | Inference rule for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | pm2.21dd 185 | A contradiction implies anything. Deduction from pm2.21 119. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 22-Jul-2019.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | pm2.65d 186 | Deduction rule for proof by contradiction. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 26-May-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | mto 187 | 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 149. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
⊢ ¬ 𝜓 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | mtod 188 | Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
⊢ (𝜑 → ¬ 𝜒) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | mtoi 189 | Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.) |
⊢ ¬ 𝜒 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | mt2 190 | A rule similar to modus tollens. Inference associated with con2i 133. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Sep-2013.) |
⊢ 𝜓 & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | mt3 191 | A rule similar to modus tollens. Inference associated with con1i 143. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
⊢ ¬ 𝜓 & ⊢ (¬ 𝜑 → 𝜓) ⇒ ⊢ 𝜑 | ||
Theorem | peirce 192 | 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 193 | The Inversion Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. Using dfor2 426, 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 83. (Contributed by NM, 12-Aug-2004.) |
⊢ (((𝜑 → 𝜓) → 𝜓) → ((𝜓 → 𝜑) → 𝜑)) | ||
Theorem | bijust 194 | Theorem used to justify definition of biconditional df-bi 196. (Contributed by NM, 11-May-1999.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |
⊢ ¬ ((¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))) | ||
The definition df-bi 196 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 384 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 195 | Extend our wff definition to include the biconditional connective. |
wff (𝜑 ↔ 𝜓) | ||
Definition | df-bi 196 |
Define the biconditional (logical 'iff').
The definition df-bi 196 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 384 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 1033) 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 194. It is impossible to use df-bi 196 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 196 in the proof with the corresponding bijust 194 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 1478) and the constant false ⊥ (df-fal 1481), we will be able to prove these truth table values: ((⊤ ↔ ⊤) ↔ ⊤) (trubitru 1511), ((⊤ ↔ ⊥) ↔ ⊥) (trubifal 1513), ((⊥ ↔ ⊤) ↔ ⊥) (falbitru 1512), and ((⊥ ↔ ⊥) ↔ ⊤) (falbifal 1514). See dfbi1 202, dfbi2 658, and dfbi3 933 for theorems suggesting typical textbook definitions of ↔, showing that our definition has the properties we expect. Theorem dfbi1 202 is particularly useful if we want to eliminate ↔ from an expression to convert it to primitives. Theorem dfbi 659 shows this definition rewritten in an abbreviated form after conjunction is introduced, for easier understanding. Contrast with ∨ (df-or 384), → (wi 4), ⊼ (df-nan 1440), and ⊻ (df-xor 1457) . In some sense ↔ returns true if two truth values are equal; = (df-cleq 2603) returns true if two classes are equal. (Contributed by NM, 27-Dec-1992.) |
⊢ ¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) | ||
Theorem | impbi 197 | Property of the biconditional connective. (Contributed by NM, 11-May-1999.) |
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → (𝜑 ↔ 𝜓))) | ||
Theorem | impbii 198 | Infer an equivalence from an implication and its converse. Inference associated with impbi 197. (Contributed by NM, 29-Dec-1992.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜓 → 𝜑) ⇒ ⊢ (𝜑 ↔ 𝜓) | ||
Theorem | impbidd 199 | Deduce an equivalence from two implications. Double deduction associated with impbi 197 and impbii 198. Deduction associated with impbid 201. (Contributed by Rodolfo Medina, 12-Oct-2010.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) | ||
Theorem | impbid21d 200 | Deduce an equivalence from two implications. (Contributed by Wolf Lammen, 12-May-2013.) |
⊢ (𝜓 → (𝜒 → 𝜃)) & ⊢ (𝜑 → (𝜃 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |