![]() |
Metamath
Proof Explorer Theorem List (p. 2 of 435) | < 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: | ![]() (1-28329) |
![]() (28330-29854) |
![]() (29855-43446) |
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 175 (the other partial converse being jarli 124). (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 139 followed by nsyl2 145, 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 | pm2.21i 117 | A contradiction implies anything. Inference associated with pm2.21 121. Its associated inference is pm2.24ii 118. (Contributed by NM, 16-Sep-1993.) |
⊢ ¬ 𝜑 ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.24ii 118 | A contradiction implies anything. Inference associated with pm2.21i 117 and pm2.24i 148. (Contributed by NM, 27-Feb-2008.) |
⊢ 𝜑 & ⊢ ¬ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | pm2.21d 119 | A contradiction implies anything. Deduction associated with pm2.21 121. (Contributed by NM, 10-Feb-1996.) |
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | pm2.21ddALT 120 | Alternate proof of pm2.21dd 187. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | pm2.21 121 | 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 122 and its associated inference is pm2.21i 117. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 14-Sep-2012.) |
⊢ (¬ 𝜑 → (𝜑 → 𝜓)) | ||
Theorem | pm2.24 122 | Theorem *2.24 of [WhiteheadRussell] p. 104. Its associated inference is pm2.24i 148. Commuted form of pm2.21 121. (Contributed by NM, 3-Jan-2005.) |
⊢ (𝜑 → (¬ 𝜑 → 𝜓)) | ||
Theorem | jarl 123 | Elimination of a nested antecedent. (Contributed by Wolf Lammen, 10-May-2013.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → (¬ 𝜑 → 𝜒)) | ||
Theorem | jarli 124 | Inference associated with jarl 123. Partial converse of ja 175 (the other partial converse being jarri 107). (Contributed by Wolf Lammen, 4-Oct-2013.) |
⊢ ((𝜑 → 𝜓) → 𝜒) ⇒ ⊢ (¬ 𝜑 → 𝜒) | ||
Theorem | pm2.18 125 | Clavius's 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 181. (Contributed by NM, 29-Dec-1992.) |
⊢ ((¬ 𝜑 → 𝜑) → 𝜑) | ||
Theorem | pm2.18i 126 | Inference associated with the Clavius law pm2.18 125. (Contributed by BJ, 30-Mar-2020.) |
⊢ (¬ 𝜑 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | pm2.18d 127 | Deduction form of the Clavius law pm2.18 125. (Contributed by FL, 12-Jul-2009.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ (𝜑 → (¬ 𝜓 → 𝜓)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | notnotr 128 | Double negation elimination. Converse of notnot 139 and one implication of notnotb 307. 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 129 | Inference associated with notnotr 128. For a shorter proof using ax-2 7, see notnotriALT 130. (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 130 |
Alternate proof of notnotri 129. Inference associated with notnotr 128.
Remark: the proof via notnotr 128 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 131 | Deduction associated with notnotr 128 and notnotri 129. Double negation elimination rule. A translation of the natural deduction rule ¬ ¬ C , Γ⊢ ¬ ¬ 𝜓 ⇒ Γ⊢ 𝜓; see natded 27817. 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 132 | A contraposition deduction. (Contributed by NM, 19-Aug-1993.) |
⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 → ¬ 𝜓)) | ||
Theorem | con2 133 | Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 12-Feb-2013.) |
⊢ ((𝜑 → ¬ 𝜓) → (𝜓 → ¬ 𝜑)) | ||
Theorem | mt2d 134 | Modus tollens deduction. (Contributed by NM, 4-Jul-1994.) |
⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | mt2i 135 | Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.) |
⊢ 𝜒 & ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | nsyl3 136 | A negated syllogism inference. (Contributed by NM, 1-Dec-1995.) |
⊢ (𝜑 → ¬ 𝜓) & ⊢ (𝜒 → 𝜓) ⇒ ⊢ (𝜒 → ¬ 𝜑) | ||
Theorem | con2i 137 | A contraposition inference. Its associated inference is mt2 192. (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 138 | A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.) |
⊢ (𝜑 → ¬ 𝜓) & ⊢ (𝜒 → 𝜓) ⇒ ⊢ (𝜑 → ¬ 𝜒) | ||
Theorem | notnot 139 | Double negation introduction. Converse of notnotr 128 and one implication of notnotb 307. 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 140 | Inference associated with notnot 139. (Contributed by NM, 27-Feb-2008.) |
⊢ 𝜑 ⇒ ⊢ ¬ ¬ 𝜑 | ||
Theorem | notnotd 141 | Deduction associated with notnot 139 and notnoti 140. (Contributed by Jarvin Udandy, 2-Sep-2016.) Avoid biconditional. (Revised by Wolf Lammen, 27-Mar-2021.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ¬ ¬ 𝜓) | ||
Theorem | con1d 142 | A contraposition deduction. (Contributed by NM, 27-Dec-1992.) |
⊢ (𝜑 → (¬ 𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (¬ 𝜒 → 𝜓)) | ||
Theorem | mt3d 143 | Modus tollens deduction. (Contributed by NM, 26-Mar-1995.) |
⊢ (𝜑 → ¬ 𝜒) & ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | mt3i 144 | Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.) |
⊢ ¬ 𝜒 & ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | nsyl2 145 | A negated syllogism inference. (Contributed by NM, 26-Jun-1994.) |
⊢ (𝜑 → ¬ 𝜓) & ⊢ (¬ 𝜒 → 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
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 193. (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 | pm2.24i 148 | Inference associated with pm2.24 122. Its associated inference is pm2.24ii 118. (Contributed by NM, 20-Aug-2001.) |
⊢ 𝜑 ⇒ ⊢ (¬ 𝜑 → 𝜓) | ||
Theorem | pm2.24d 149 | Deduction form of pm2.24 122. (Contributed by NM, 30-Jan-2006.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) | ||
Theorem | con3d 150 | A contraposition deduction. Deduction form of con3 151. (Contributed by NM, 10-Jan-1993.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) | ||
Theorem | con3 151 | 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 152. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 13-Feb-2013.) |
⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑)) | ||
Theorem | con3i 152 | A contraposition inference. Inference associated with con3 151. Its associated inference is mto 189. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (¬ 𝜓 → ¬ 𝜑) | ||
Theorem | con3rr3 153 | Rotate through consequent right. (Contributed by Wolf Lammen, 3-Nov-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (¬ 𝜒 → (𝜑 → ¬ 𝜓)) | ||
Theorem | mt4d 154 | Modus tollens deduction. Deduction form of mt4 116. (Contributed by NM, 9-Jun-2006.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | mt4i 155 | Modus tollens inference. (Contributed by Wolf Lammen, 12-May-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 | pm3.2im 159 | 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 160 | Theorem 8 of [Margaris] p. 60. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |
⊢ (𝜑 → (¬ 𝜓 → ¬ (𝜑 → 𝜓))) | ||
Theorem | jc 161 | Deduction joining the consequents of two premises. A deduction associated with pm3.2im 159. (Contributed by NM, 28-Dec-1992.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → ¬ (𝜓 → ¬ 𝜒)) | ||
Theorem | impi 162 | An importation inference. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 20-Jul-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (¬ (𝜑 → ¬ 𝜓) → 𝜒) | ||
Theorem | expi 163 | An exportation inference. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) |
⊢ (¬ (𝜑 → ¬ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | simprim 164 | 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 165 | 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 166 | Theorem *2.5 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 9-Oct-2012.) |
⊢ (¬ (𝜑 → 𝜓) → (¬ 𝜑 → 𝜓)) | ||
Theorem | pm2.51 167 | Theorem *2.51 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (𝜑 → 𝜓) → (𝜑 → ¬ 𝜓)) | ||
Theorem | pm2.521 168 | Theorem *2.521 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 8-Oct-2012.) |
⊢ (¬ (𝜑 → 𝜓) → (𝜓 → 𝜑)) | ||
Theorem | pm2.52 169 | Theorem *2.52 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 8-Oct-2012.) |
⊢ (¬ (𝜑 → 𝜓) → (¬ 𝜑 → ¬ 𝜓)) | ||
Theorem | expt 170 | Exportation theorem ex 403 expressed with primitive connectives. (Contributed by NM, 28-Dec-1992.) |
⊢ ((¬ (𝜑 → ¬ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒))) | ||
Theorem | impt 171 | Importation theorem imp 397 expressed with primitive connectives. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jul-2013.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (¬ (𝜑 → ¬ 𝜓) → 𝜒)) | ||
Theorem | pm2.61d 172 | Deduction eliminating an antecedent. (Contributed by NM, 27-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | pm2.61d1 173 | Inference eliminating an antecedent. (Contributed by NM, 15-Jul-2005.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (¬ 𝜓 → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | pm2.61d2 174 | Inference eliminating an antecedent. (Contributed by NM, 18-Aug-1993.) |
⊢ (𝜑 → (¬ 𝜓 → 𝜒)) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | ja 175 | Inference joining the antecedents of two premises. For partial converses, see jarri 107 and jarli 124. (Contributed by NM, 24-Jan-1993.) (Proof shortened by Mel L. O'Cat, 19-Feb-2008.) |
⊢ (¬ 𝜑 → 𝜒) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ ((𝜑 → 𝜓) → 𝜒) | ||
Theorem | jad 176 | Deduction form of ja 175. (Contributed by Scott Fenton, 13-Dec-2010.) (Proof shortened by Andrew Salmon, 17-Sep-2011.) |
⊢ (𝜑 → (¬ 𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜒 → 𝜃)) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜒) → 𝜃)) | ||
Theorem | pm2.61i 177 | Inference eliminating an antecedent. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.) |
⊢ (𝜑 → 𝜓) & ⊢ (¬ 𝜑 → 𝜓) ⇒ ⊢ 𝜓 | ||
Theorem | pm2.61ii 178 | Inference eliminating two antecedents. (Contributed by NM, 4-Jan-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) |
⊢ (¬ 𝜑 → (¬ 𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | pm2.61nii 179 | 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 180 | Inference eliminating three antecedents. (Contributed by NM, 2-Jan-2002.) (Proof shortened by Wolf Lammen, 22-Sep-2013.) |
⊢ (¬ 𝜑 → (¬ 𝜓 → (¬ 𝜒 → 𝜃))) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜓 → 𝜃) & ⊢ (𝜒 → 𝜃) ⇒ ⊢ 𝜃 | ||
Theorem | pm2.01 181 | 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 125. (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 182 | Deduction based on reductio ad absurdum. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Mar-2013.) |
⊢ (𝜑 → (𝜓 → ¬ 𝜓)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | pm2.6 183 | Theorem *2.6 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
⊢ ((¬ 𝜑 → 𝜓) → ((𝜑 → 𝜓) → 𝜓)) | ||
Theorem | pm2.61 184 | 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 185 | 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 186 | Inference for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | pm2.21dd 187 | A contradiction implies anything. Deduction from pm2.21 121. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 22-Jul-2019.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | pm2.65d 188 | Deduction for proof by contradiction. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 26-May-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | mto 189 | 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 152. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
⊢ ¬ 𝜓 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | mtod 190 | Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) |
⊢ (𝜑 → ¬ 𝜒) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | mtoi 191 | Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.) |
⊢ ¬ 𝜒 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | mt2 192 | A rule similar to modus tollens. Inference associated with con2i 137. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Sep-2013.) |
⊢ 𝜓 & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | mt3 193 | 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.) |
⊢ ¬ 𝜓 & ⊢ (¬ 𝜑 → 𝜓) ⇒ ⊢ 𝜑 | ||
Theorem | peirce 194 | Peirce's axiom. A non-intuitionistic implication-only statement. Added to intuitionistic (implicational) propositional calculus, it gives classical (implicational) propositional calculus. For another non-intuitionistic positive statement, see curryax 924. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 9-Oct-2012.) |
⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜑) | ||
Theorem | looinv 195 | The Inversion Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. Using dfor2 932, 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 | bijust0 196 | A self-implication (see id 22) does not imply its own negation. The justification theorem bijust 197 is one of its instances. (Contributed by NM, 11-May-1999.) (Proof shortened by Josh Purinton, 29-Dec-2000.) Extract bijust0 196 from proof of bijust 197. (Revised by BJ, 19-Mar-2020.) |
⊢ ¬ ((𝜑 → 𝜑) → ¬ (𝜑 → 𝜑)) | ||
Theorem | bijust 197 | Theorem used to justify the definition of the biconditional df-bi 199. Instance of bijust0 196. (Contributed by NM, 11-May-1999.) |
⊢ ¬ ((¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))) | ||
The definition df-bi 199 in this section is our first definition, which introduces and defines the biconditional connective ↔ used to denote logical equivalence. 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 881 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. A note on definitions: definitions are required to be eliminable (that is, a theorem stated in terms of the defined symbol can also be stated without it) and conservative (that is, a theorem whose statement does not contain the defined symbol can be proved without using that definition). This means that a definition does not increase the expressive power nor the deductive power, respectively, of a theory. On the other hand, definitions are often useful to write shorter proofs, so in (i)set.mm we will generally not try to avoid them. This is why, for instance, some theorems which do not contain disjunction in their statement are placed after the section on disjunction because a shorter proof using disjunction is possible. | ||
Syntax | wb 198 | Extend wff definition to include the biconditional connective. |
wff (𝜑 ↔ 𝜓) | ||
Definition | df-bi 199 |
Define the biconditional (logical "iff" or "if and only
if").
The definition df-bi 199 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 881 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 1115) 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 197. It is impossible to use df-bi 199 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 199 in the proof with the corresponding bijust 197 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 1662) and the constant false ⊥ (df-fal 1672), we will be able to prove these truth table values: ((⊤ ↔ ⊤) ↔ ⊤) (trubitru 1688), ((⊤ ↔ ⊥) ↔ ⊥) (trubifal 1690), ((⊥ ↔ ⊤) ↔ ⊥) (falbitru 1689), and ((⊥ ↔ ⊥) ↔ ⊤) (falbifal 1691). See dfbi1 205, dfbi2 468, and dfbi3 1078 for theorems suggesting typical textbook definitions of ↔, showing that our definition has the properties we expect. Theorem dfbi1 205 is particularly useful if we want to eliminate ↔ from an expression to convert it to primitives. Theorem dfbi 469 shows this definition rewritten in an abbreviated form after conjunction is introduced, for easier understanding. Contrast with ∨ (df-or 881), → (wi 4), ⊼ (df-nan 1615), and ⊻ (df-xor 1640). In some sense ↔ returns true if two truth values are equal; = (df-cleq 2817) returns true if two classes are equal. (Contributed by NM, 27-Dec-1992.) |
⊢ ¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) | ||
Theorem | impbi 200 | Property of the biconditional connective. (Contributed by NM, 11-May-1999.) |
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜑) → (𝜑 ↔ 𝜓))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |