Home | Metamath
Proof Explorer Theorem List (p. 2 of 464) | < 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-29181) |
Hilbert Space Explorer
(29182-30704) |
Users' Mathboxes
(30705-46395) |
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. Sometimes called "Syll-Simp" since it is a syllogism applied to ax-1 6 ("Simplification"). (Contributed by Wolf Lammen, 9-May-2013.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒)) | ||
Theorem | jarri 107 | Inference associated with jarr 106. Partial converse of ja 186 (the other partial converse being jarli 126). (Contributed by Wolf Lammen, 20-Sep-2013.) |
⊢ ((𝜑 → 𝜓) → 𝜒) ⇒ ⊢ (𝜓 → 𝜒) | ||
Theorem | pm2.86d 108 | Deduction associated with pm2.86 109. (Contributed by NM, 29-Jun-1995.) (Proof shortened by Wolf Lammen, 3-Apr-2013.) |
⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | ||
Theorem | pm2.86 109 | 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 110 | Inference associated with pm2.86 109. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Apr-2013.) |
⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | loolin 111 | The Linearity Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. See loowoz 112 for an alternate axiom. (Contributed by Mel L. O'Cat, 12-Aug-2004.) |
⊢ (((𝜑 → 𝜓) → (𝜓 → 𝜑)) → (𝜓 → 𝜑)) | ||
Theorem | loowoz 112 | An alternate for the Linearity Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz loolin 111, 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. It introduces logical negation. | ||
Theorem | con4 113 | Alias for ax-3 8 to be used instead of it for labeling consistency. Its associated inference is con4i 114 and its associated deduction is con4d 115. (Contributed by BJ, 24-Dec-2020.) |
⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑)) | ||
Theorem | con4i 114 |
Inference associated with con4 113. Its associated inference is mt4 116.
Remark: this can also be proved using notnot 142 followed by nsyl2 141, 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 115 | Deduction associated with con4 113. (Contributed by NM, 26-Mar-1995.) |
⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 → 𝜓)) | ||
Theorem | mt4 116 | The rule of modus tollens. Inference associated with con4i 114. (Contributed by Wolf Lammen, 12-May-2013.) |
⊢ 𝜑 & ⊢ (¬ 𝜓 → ¬ 𝜑) ⇒ ⊢ 𝜓 | ||
Theorem | mt4d 117 | Modus tollens deduction. Deduction form of mt4 116. (Contributed by NM, 9-Jun-2006.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | mt4i 118 | Modus tollens inference. (Contributed by Wolf Lammen, 12-May-2013.) |
⊢ 𝜒 & ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.21i 119 | A contradiction implies anything. Inference associated with pm2.21 123. Its associated inference is pm2.24ii 120. (Contributed by NM, 16-Sep-1993.) |
⊢ ¬ 𝜑 ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.24ii 120 | A contradiction implies anything. Inference associated with pm2.21i 119 and pm2.24i 150. (Contributed by NM, 27-Feb-2008.) |
⊢ 𝜑 & ⊢ ¬ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | pm2.21d 121 | A contradiction implies anything. Deduction associated with pm2.21 123. (Contributed by NM, 10-Feb-1996.) |
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | pm2.21ddALT 122 | Alternate proof of pm2.21dd 194. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | pm2.21 123 | From a wff and its negation, anything follows. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law. Its commuted form is pm2.24 124 and its associated inference is pm2.21i 119. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 14-Sep-2012.) |
⊢ (¬ 𝜑 → (𝜑 → 𝜓)) | ||
Theorem | pm2.24 124 | Theorem *2.24 of [WhiteheadRussell] p. 104. Its associated inference is pm2.24i 150. Commuted form of pm2.21 123. (Contributed by NM, 3-Jan-2005.) |
⊢ (𝜑 → (¬ 𝜑 → 𝜓)) | ||
Theorem | jarl 125 | Elimination of a nested antecedent. (Contributed by Wolf Lammen, 10-May-2013.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → (¬ 𝜑 → 𝜒)) | ||
Theorem | jarli 126 | Inference associated with jarl 125. Partial converse of ja 186 (the other partial converse being jarri 107). (Contributed by Wolf Lammen, 4-Oct-2013.) |
⊢ ((𝜑 → 𝜓) → 𝜒) ⇒ ⊢ (¬ 𝜑 → 𝜒) | ||
Theorem | pm2.18d 127 | Deduction form of the Clavius law pm2.18 128. (Contributed by FL, 12-Jul-2009.) (Proof shortened by Andrew Salmon, 7-May-2011.) Revised to shorten pm2.18 128. (Revised by Wolf Lammen, 17-Nov-2023.) |
⊢ (𝜑 → (¬ 𝜓 → 𝜓)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.18 128 | Clavius law, or "consequentia mirabilis" ("admirable consequence"). If a formula is implied by its negation, then it is true. Can be used in proofs by contradiction. Theorem *2.18 of [WhiteheadRussell] p. 103. See also the weak Clavius law pm2.01 188. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 17-Nov-2023.) |
⊢ ((¬ 𝜑 → 𝜑) → 𝜑) | ||
Theorem | pm2.18i 129 | Inference associated with the Clavius law pm2.18 128. (Contributed by BJ, 30-Mar-2020.) |
⊢ (¬ 𝜑 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | notnotr 130 | Double negation elimination. Converse of notnot 142 and one implication of notnotb 314. 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 131 | Inference associated with notnotr 130. For a shorter proof using ax-2 7, see notnotriALT 132. (Contributed by NM, 27-Feb-2008.) (Proof shortened by Wolf Lammen, 15-Jul-2021.) Remove dependency on ax-2 7. (Revised by Steven Nguyen, 27-Dec-2022.) |
⊢ ¬ ¬ 𝜑 ⇒ ⊢ 𝜑 | ||
Theorem | notnotriALT 132 | Alternate proof of notnotri 131. The proof via notnotr 130 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 ¬ ¬ 𝜑 once, whereas the present proof has to construct the formula 𝜑 twice and the formula ¬ 𝜑 once, and therefore makes only one use of wn 3 instead of two. This can be checked by running the Metamath command "MM> SHOW PROOF notnotri / NORMAL". (Contributed by NM, 27-Feb-2008.) (Proof shortened by Wolf Lammen, 15-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ ¬ 𝜑 ⇒ ⊢ 𝜑 | ||
Theorem | notnotrd 133 | Deduction associated with notnotr 130 and notnotri 131. Double negation elimination rule. A translation of the natural deduction rule ¬ ¬ C , Γ⊢ ¬ ¬ 𝜓 ⇒ Γ⊢ 𝜓; see natded 28668. 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 134 | A contraposition deduction. (Contributed by NM, 19-Aug-1993.) |
⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 → ¬ 𝜓)) | ||
Theorem | con2 135 | Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 12-Feb-2013.) |
⊢ ((𝜑 → ¬ 𝜓) → (𝜓 → ¬ 𝜑)) | ||
Theorem | mt2d 136 | Modus tollens deduction. (Contributed by NM, 4-Jul-1994.) |
⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | mt2i 137 | Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.) |
⊢ 𝜒 & ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | nsyl3 138 | A negated syllogism inference. (Contributed by NM, 1-Dec-1995.) |
⊢ (𝜑 → ¬ 𝜓) & ⊢ (𝜒 → 𝜓) ⇒ ⊢ (𝜒 → ¬ 𝜑) | ||
Theorem | con2i 139 | A contraposition inference. Its associated inference is mt2 199. (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 140 | A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.) |
⊢ (𝜑 → ¬ 𝜓) & ⊢ (𝜒 → 𝜓) ⇒ ⊢ (𝜑 → ¬ 𝜒) | ||
Theorem | nsyl2 141 | A negated syllogism inference. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 14-Nov-2023.) |
⊢ (𝜑 → ¬ 𝜓) & ⊢ (¬ 𝜒 → 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | notnot 142 | Double negation introduction. Converse of notnotr 130 and one implication of notnotb 314. 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 143 | Inference associated with notnot 142. (Contributed by NM, 27-Feb-2008.) |
⊢ 𝜑 ⇒ ⊢ ¬ ¬ 𝜑 | ||
Theorem | notnotd 144 | Deduction associated with notnot 142 and notnoti 143. (Contributed by Jarvin Udandy, 2-Sep-2016.) Avoid biconditional. (Revised by Wolf Lammen, 27-Mar-2021.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ¬ ¬ 𝜓) | ||
Theorem | con1d 145 | A contraposition deduction. (Contributed by NM, 27-Dec-1992.) |
⊢ (𝜑 → (¬ 𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (¬ 𝜒 → 𝜓)) | ||
Theorem | con1 146 | Contraposition. Theorem *2.15 of [WhiteheadRussell] p. 102. Its associated inference is con1i 147. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 12-Feb-2013.) |
⊢ ((¬ 𝜑 → 𝜓) → (¬ 𝜓 → 𝜑)) | ||
Theorem | con1i 147 | A contraposition inference. Inference associated with con1 146. Its associated inference is mt3 200. (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 | mt3d 148 | Modus tollens deduction. (Contributed by NM, 26-Mar-1995.) |
⊢ (𝜑 → ¬ 𝜒) & ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | mt3i 149 | Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.) |
⊢ ¬ 𝜒 & ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.24i 150 | Inference associated with pm2.24 124. Its associated inference is pm2.24ii 120. (Contributed by NM, 20-Aug-2001.) |
⊢ 𝜑 ⇒ ⊢ (¬ 𝜑 → 𝜓) | ||
Theorem | pm2.24d 151 | Deduction form of pm2.24 124. (Contributed by NM, 30-Jan-2006.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) | ||
Theorem | con3d 152 | A contraposition deduction. Deduction form of con3 153. (Contributed by NM, 10-Jan-1993.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) | ||
Theorem | con3 153 | 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 154. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 13-Feb-2013.) |
⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑)) | ||
Theorem | con3i 154 | A contraposition inference. Inference associated with con3 153. Its associated inference is mto 196. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (¬ 𝜓 → ¬ 𝜑) | ||
Theorem | con3rr3 155 | Rotate through consequent right. (Contributed by Wolf Lammen, 3-Nov-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (¬ 𝜒 → (𝜑 → ¬ 𝜓)) | ||
Theorem | nsyld 156 | A negated syllogism deduction. (Contributed by NM, 9-Apr-2005.) |
⊢ (𝜑 → (𝜓 → ¬ 𝜒)) & ⊢ (𝜑 → (𝜏 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ¬ 𝜏)) | ||
Theorem | nsyli 157 | A negated syllogism inference. (Contributed by NM, 3-May-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → ¬ 𝜒) ⇒ ⊢ (𝜑 → (𝜃 → ¬ 𝜓)) | ||
Theorem | nsyl4 158 | A negated syllogism inference. (Contributed by NM, 15-Feb-1996.) |
⊢ (𝜑 → 𝜓) & ⊢ (¬ 𝜑 → 𝜒) ⇒ ⊢ (¬ 𝜒 → 𝜓) | ||
Theorem | nsyl5 159 | A negated syllogism inference. (Contributed by Wolf Lammen, 20-May-2024.) |
⊢ (𝜑 → 𝜓) & ⊢ (¬ 𝜑 → 𝜒) ⇒ ⊢ (¬ 𝜓 → 𝜒) | ||
Theorem | pm3.2im 160 | Theorem *3.2 of [WhiteheadRussell] p. 111, expressed with primitive connectives (see pm3.2 469). (Contributed by NM, 29-Dec-1992.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |
⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓))) | ||
Theorem | jc 161 | Deduction joining the consequents of two premises. A deduction associated with pm3.2im 160. (Contributed by NM, 28-Dec-1992.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → ¬ (𝜓 → ¬ 𝜒)) | ||
Theorem | jcn 162 | Theorem joining the consequents of two premises. Theorem 8 of [Margaris] p. 60. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |
⊢ (𝜑 → (¬ 𝜓 → ¬ (𝜑 → 𝜓))) | ||
Theorem | jcnd 163 | Deduction joining the consequents of two premises. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by Wolf Lammen, 10-Apr-2024.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → ¬ 𝜒) ⇒ ⊢ (𝜑 → ¬ (𝜓 → 𝜒)) | ||
Theorem | impi 164 | An importation inference. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 20-Jul-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (¬ (𝜑 → ¬ 𝜓) → 𝜒) | ||
Theorem | expi 165 | An exportation inference. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) |
⊢ (¬ (𝜑 → ¬ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | simprim 166 | 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 167 | 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.5g 168 | General instance of Theorem *2.5 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 9-Oct-2012.) |
⊢ (¬ (𝜑 → 𝜓) → (¬ 𝜑 → 𝜒)) | ||
Theorem | pm2.5 169 | Theorem *2.5 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (𝜑 → 𝜓) → (¬ 𝜑 → 𝜓)) | ||
Theorem | conax1 170 | Contrapositive of ax-1 6. (Contributed by BJ, 28-Oct-2023.) |
⊢ (¬ (𝜑 → 𝜓) → ¬ 𝜓) | ||
Theorem | conax1k 171 | Weakening of conax1 170. General instance of pm2.51 172 and of pm2.52 173. (Contributed by BJ, 28-Oct-2023.) |
⊢ (¬ (𝜑 → 𝜓) → (𝜒 → ¬ 𝜓)) | ||
Theorem | pm2.51 172 | Theorem *2.51 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (𝜑 → 𝜓) → (𝜑 → ¬ 𝜓)) | ||
Theorem | pm2.52 173 | Theorem *2.52 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 8-Oct-2012.) |
⊢ (¬ (𝜑 → 𝜓) → (¬ 𝜑 → ¬ 𝜓)) | ||
Theorem | pm2.521g 174 | A general instance of Theorem *2.521 of [WhiteheadRussell] p. 107. (Contributed by BJ, 28-Oct-2023.) |
⊢ (¬ (𝜑 → 𝜓) → (𝜓 → 𝜒)) | ||
Theorem | pm2.521g2 175 | A general instance of Theorem *2.521 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 8-Oct-2012.) |
⊢ (¬ (𝜑 → 𝜓) → (𝜒 → 𝜑)) | ||
Theorem | pm2.521 176 | Theorem *2.521 of [WhiteheadRussell] p. 107. Instance of pm2.521g 174 and of pm2.521g2 175. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (𝜑 → 𝜓) → (𝜓 → 𝜑)) | ||
Theorem | expt 177 | Exportation theorem pm3.3 448 (closed form of ex 412) expressed with primitive connectives. (Contributed by NM, 28-Dec-1992.) |
⊢ ((¬ (𝜑 → ¬ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒))) | ||
Theorem | impt 178 | Importation theorem pm3.1 988 (closed form of imp 406) expressed with primitive connectives. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jul-2013.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (¬ (𝜑 → ¬ 𝜓) → 𝜒)) | ||
Theorem | pm2.61d 179 | Deduction eliminating an antecedent. (Contributed by NM, 27-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | pm2.61d1 180 | Inference eliminating an antecedent. (Contributed by NM, 15-Jul-2005.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (¬ 𝜓 → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | pm2.61d2 181 | Inference eliminating an antecedent. (Contributed by NM, 18-Aug-1993.) |
⊢ (𝜑 → (¬ 𝜓 → 𝜒)) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | pm2.61i 182 | Inference eliminating an antecedent. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2023.) |
⊢ (𝜑 → 𝜓) & ⊢ (¬ 𝜑 → 𝜓) ⇒ ⊢ 𝜓 | ||
Theorem | pm2.61ii 183 | Inference eliminating two antecedents. (Contributed by NM, 4-Jan-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |
⊢ (¬ 𝜑 → (¬ 𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | pm2.61nii 184 | 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 185 | Inference eliminating three antecedents. (Contributed by NM, 2-Jan-2002.) (Proof shortened by Wolf Lammen, 22-Sep-2013.) |
⊢ (¬ 𝜑 → (¬ 𝜓 → (¬ 𝜒 → 𝜃))) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜓 → 𝜃) & ⊢ (𝜒 → 𝜃) ⇒ ⊢ 𝜃 | ||
Theorem | ja 186 | Inference joining the antecedents of two premises. For partial converses, see jarri 107 and jarli 126. (Contributed by NM, 24-Jan-1993.) (Proof shortened by Mel L. O'Cat, 19-Feb-2008.) |
⊢ (¬ 𝜑 → 𝜒) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ ((𝜑 → 𝜓) → 𝜒) | ||
Theorem | jad 187 | Deduction form of ja 186. (Contributed by Scott Fenton, 13-Dec-2010.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ (𝜑 → (¬ 𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜒 → 𝜃)) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜒) → 𝜃)) | ||
Theorem | pm2.01 188 | Weak Clavius law. If a formula implies its negation, then it is false. A form of "reductio ad absurdum", which can be used in proofs by contradiction. Theorem *2.01 of [WhiteheadRussell] p. 100. Provable in minimal calculus, contrary to the Clavius law pm2.18 128. (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 189 | Deduction based on reductio ad absurdum. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Mar-2013.) |
⊢ (𝜑 → (𝜓 → ¬ 𝜓)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | pm2.6 190 | Theorem *2.6 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
⊢ ((¬ 𝜑 → 𝜓) → ((𝜑 → 𝜓) → 𝜓)) | ||
Theorem | pm2.61 191 | 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 192 | 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 193 | Inference for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | pm2.21dd 194 | A contradiction implies anything. Deduction from pm2.21 123. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 22-Jul-2019.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | pm2.65d 195 | Deduction for proof by contradiction. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 26-May-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | mto 196 | 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 154. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
⊢ ¬ 𝜓 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | mtod 197 | Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
⊢ (𝜑 → ¬ 𝜒) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | mtoi 198 | Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.) |
⊢ ¬ 𝜒 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | mt2 199 | A rule similar to modus tollens. Inference associated with con2i 139. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Sep-2013.) |
⊢ 𝜓 & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | mt3 200 | A rule similar to modus tollens. Inference associated with con1i 147. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
⊢ ¬ 𝜓 & ⊢ (¬ 𝜑 → 𝜓) ⇒ ⊢ 𝜑 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |