Home | Metamath
Proof Explorer Theorem List (p. 4 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 3bitr2ri 301 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ (𝜃 ↔ 𝜑) | ||
Theorem | 3bitr3i 302 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜑 ↔ 𝜒) & ⊢ (𝜓 ↔ 𝜃) ⇒ ⊢ (𝜒 ↔ 𝜃) | ||
Theorem | 3bitr3ri 303 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜑 ↔ 𝜒) & ⊢ (𝜓 ↔ 𝜃) ⇒ ⊢ (𝜃 ↔ 𝜒) | ||
Theorem | 3bitr4i 304 | A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜓) ⇒ ⊢ (𝜒 ↔ 𝜃) | ||
Theorem | 3bitr4ri 305 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜓) ⇒ ⊢ (𝜃 ↔ 𝜒) | ||
Theorem | 3bitrd 306 | Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜒 ↔ 𝜃)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜏)) | ||
Theorem | 3bitrrd 307 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜒 ↔ 𝜃)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜏 ↔ 𝜓)) | ||
Theorem | 3bitr2d 308 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜏)) | ||
Theorem | 3bitr2rd 309 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜏 ↔ 𝜓)) | ||
Theorem | 3bitr3d 310 | Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜓 ↔ 𝜃)) & ⊢ (𝜑 → (𝜒 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | ||
Theorem | 3bitr3rd 311 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜓 ↔ 𝜃)) & ⊢ (𝜑 → (𝜒 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜏 ↔ 𝜃)) | ||
Theorem | 3bitr4d 312 | Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 18-Oct-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜓)) & ⊢ (𝜑 → (𝜏 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | ||
Theorem | 3bitr4rd 313 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜓)) & ⊢ (𝜑 → (𝜏 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜏 ↔ 𝜃)) | ||
Theorem | 3bitr3g 314 | More general version of 3bitr3i 302. Useful for converting definitions in a formula. (Contributed by NM, 4-Jun-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜓 ↔ 𝜃) & ⊢ (𝜒 ↔ 𝜏) ⇒ ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | ||
Theorem | 3bitr4g 315 | More general version of 3bitr4i 304. Useful for converting definitions in a formula. (Contributed by NM, 11-May-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 ↔ 𝜓) & ⊢ (𝜏 ↔ 𝜒) ⇒ ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | ||
Theorem | notnotb 316 | Double negation. Theorem *4.13 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 ↔ ¬ ¬ 𝜑) | ||
Theorem | con34b 317 | A biconditional form of contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116. (Contributed by NM, 11-May-1993.) |
⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜓 → ¬ 𝜑)) | ||
Theorem | con4bid 318 | A contraposition deduction. (Contributed by NM, 21-May-1994.) |
⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | notbid 319 | Deduction negating both sides of a logical equivalence. (Contributed by NM, 21-May-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒)) | ||
Theorem | notbi 320 | Contraposition. Theorem *4.11 of [WhiteheadRussell] p. 117. (Contributed by NM, 21-May-1994.) (Proof shortened by Wolf Lammen, 12-Jun-2013.) |
⊢ ((𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓)) | ||
Theorem | notbii 321 | Negate both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (¬ 𝜑 ↔ ¬ 𝜓) | ||
Theorem | con4bii 322 | A contraposition inference. (Contributed by NM, 21-May-1994.) |
⊢ (¬ 𝜑 ↔ ¬ 𝜓) ⇒ ⊢ (𝜑 ↔ 𝜓) | ||
Theorem | mtbi 323 | An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Oct-2012.) |
⊢ ¬ 𝜑 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ¬ 𝜓 | ||
Theorem | mtbir 324 | An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 14-Oct-2012.) |
⊢ ¬ 𝜓 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ¬ 𝜑 | ||
Theorem | mtbid 325 | A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.) |
⊢ (𝜑 → ¬ 𝜓) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜒) | ||
Theorem | mtbird 326 | A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 10-May-1994.) |
⊢ (𝜑 → ¬ 𝜒) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | mtbii 327 | An inference from a biconditional, similar to modus tollens. (Contributed by NM, 27-Nov-1995.) |
⊢ ¬ 𝜓 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜒) | ||
Theorem | mtbiri 328 | An inference from a biconditional, similar to modus tollens. (Contributed by NM, 24-Aug-1995.) |
⊢ ¬ 𝜒 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | sylnib 329 | A mixed syllogism inference from an implication and a biconditional. (Contributed by Wolf Lammen, 16-Dec-2013.) |
⊢ (𝜑 → ¬ 𝜓) & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (𝜑 → ¬ 𝜒) | ||
Theorem | sylnibr 330 | A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.) |
⊢ (𝜑 → ¬ 𝜓) & ⊢ (𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 → ¬ 𝜒) | ||
Theorem | sylnbi 331 | A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (¬ 𝜓 → 𝜒) ⇒ ⊢ (¬ 𝜑 → 𝜒) | ||
Theorem | sylnbir 332 | A mixed syllogism inference from a biconditional and an implication. (Contributed by Wolf Lammen, 16-Dec-2013.) |
⊢ (𝜓 ↔ 𝜑) & ⊢ (¬ 𝜓 → 𝜒) ⇒ ⊢ (¬ 𝜑 → 𝜒) | ||
Theorem | xchnxbi 333 | Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.) |
⊢ (¬ 𝜑 ↔ 𝜓) & ⊢ (𝜑 ↔ 𝜒) ⇒ ⊢ (¬ 𝜒 ↔ 𝜓) | ||
Theorem | xchnxbir 334 | Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.) |
⊢ (¬ 𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜑) ⇒ ⊢ (¬ 𝜒 ↔ 𝜓) | ||
Theorem | xchbinx 335 | Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.) |
⊢ (𝜑 ↔ ¬ 𝜓) & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (𝜑 ↔ ¬ 𝜒) | ||
Theorem | xchbinxr 336 | Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.) |
⊢ (𝜑 ↔ ¬ 𝜓) & ⊢ (𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 ↔ ¬ 𝜒) | ||
Theorem | imbi2i 337 | Introduce an antecedent to both sides of a logical equivalence. This and the next three rules are useful for building up wff's around a definition, in order to make use of the definition. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 6-Feb-2013.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓)) | ||
Theorem | jcn 338 | Inference joining the consequents of two premises. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → ¬ 𝜒) ⇒ ⊢ (𝜑 → ¬ (𝜓 → 𝜒)) | ||
Theorem | bibi2i 339 | Inference adding a biconditional to the left in an equivalence. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 16-May-2013.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓)) | ||
Theorem | bibi1i 340 | Inference adding a biconditional to the right in an equivalence. (Contributed by NM, 26-May-1993.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒)) | ||
Theorem | bibi12i 341 | The equivalence of two equivalences. (Contributed by NM, 26-May-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜃)) | ||
Theorem | imbi2d 342 | Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 → 𝜓) ↔ (𝜃 → 𝜒))) | ||
Theorem | imbi1d 343 | Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃))) | ||
Theorem | bibi2d 344 | Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒))) | ||
Theorem | bibi1d 345 | Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 11-May-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃))) | ||
Theorem | imbi12d 346 | Deduction joining two equivalences to form equivalence of implications. (Contributed by NM, 16-May-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏))) | ||
Theorem | bibi12d 347 | Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 26-May-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏))) | ||
Theorem | imbi12 348 | Closed form of imbi12i 352. Was automatically derived from its "Virtual Deduction" version and the Metamath program "MM-PA> MINIMIZE_WITH *" command. (Contributed by Alan Sare, 18-Mar-2012.) |
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)))) | ||
Theorem | imbi1 349 | Theorem *4.84 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))) | ||
Theorem | imbi2 350 | Theorem *4.85 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 19-May-2013.) |
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))) | ||
Theorem | imbi1i 351 | Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)) | ||
Theorem | imbi12i 352 | Join two logical equivalences to form equivalence of implications. (Contributed by NM, 1-Aug-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)) | ||
Theorem | bibi1 353 | Theorem *4.86 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒))) | ||
Theorem | bitr3 354 | Closed nested implication form of bitr3i 278. Derived automatically from bitr3VD 41063. (Contributed by Alan Sare, 31-Dec-2011.) |
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ↔ 𝜒) → (𝜓 ↔ 𝜒))) | ||
Theorem | con2bi 355 | Contraposition. Theorem *4.12 of [WhiteheadRussell] p. 117. (Contributed by NM, 15-Apr-1995.) (Proof shortened by Wolf Lammen, 3-Jan-2013.) |
⊢ ((𝜑 ↔ ¬ 𝜓) ↔ (𝜓 ↔ ¬ 𝜑)) | ||
Theorem | con2bid 356 | A contraposition deduction. (Contributed by NM, 15-Apr-1995.) |
⊢ (𝜑 → (𝜓 ↔ ¬ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓)) | ||
Theorem | con1bid 357 | A contraposition deduction. (Contributed by NM, 9-Oct-1999.) |
⊢ (𝜑 → (¬ 𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (¬ 𝜒 ↔ 𝜓)) | ||
Theorem | con1bii 358 | A contraposition inference. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.) |
⊢ (¬ 𝜑 ↔ 𝜓) ⇒ ⊢ (¬ 𝜓 ↔ 𝜑) | ||
Theorem | con2bii 359 | A contraposition inference. (Contributed by NM, 12-Mar-1993.) |
⊢ (𝜑 ↔ ¬ 𝜓) ⇒ ⊢ (𝜓 ↔ ¬ 𝜑) | ||
Theorem | con1b 360 | Contraposition. Bidirectional version of con1 148. (Contributed by NM, 3-Jan-1993.) |
⊢ ((¬ 𝜑 → 𝜓) ↔ (¬ 𝜓 → 𝜑)) | ||
Theorem | con2b 361 | Contraposition. Bidirectional version of con2 137. (Contributed by NM, 12-Mar-1993.) |
⊢ ((𝜑 → ¬ 𝜓) ↔ (𝜓 → ¬ 𝜑)) | ||
Theorem | biimt 362 | A wff is equivalent to itself with true antecedent. (Contributed by NM, 28-Jan-1996.) |
⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓))) | ||
Theorem | pm5.5 363 | Theorem *5.5 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
⊢ (𝜑 → ((𝜑 → 𝜓) ↔ 𝜓)) | ||
Theorem | a1bi 364 | Inference introducing a theorem as an antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Nov-2012.) |
⊢ 𝜑 ⇒ ⊢ (𝜓 ↔ (𝜑 → 𝜓)) | ||
Theorem | mt2bi 365 | A false consequent falsifies an antecedent. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.) |
⊢ 𝜑 ⇒ ⊢ (¬ 𝜓 ↔ (𝜓 → ¬ 𝜑)) | ||
Theorem | mtt 366 | Modus-tollens-like theorem. (Contributed by NM, 7-Apr-2001.) (Proof shortened by Wolf Lammen, 12-Nov-2012.) |
⊢ (¬ 𝜑 → (¬ 𝜓 ↔ (𝜓 → 𝜑))) | ||
Theorem | imnot 367 | If a proposition is false, then implying it is equivalent to being false. One of four theorems that can be used to simplify an implication (𝜑 → 𝜓), the other ones being ax-1 6 (true consequent), pm2.21 123 (false antecedent), pm5.5 363 (true antecedent). (Contributed by Mario Carneiro, 26-Apr-2019.) (Proof shortened by Wolf Lammen, 26-May-2019.) |
⊢ (¬ 𝜓 → ((𝜑 → 𝜓) ↔ ¬ 𝜑)) | ||
Theorem | pm5.501 368 | Theorem *5.501 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
⊢ (𝜑 → (𝜓 ↔ (𝜑 ↔ 𝜓))) | ||
Theorem | ibib 369 | Implication in terms of implication and biconditional. (Contributed by NM, 31-Mar-1994.) (Proof shortened by Wolf Lammen, 24-Jan-2013.) |
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → (𝜑 ↔ 𝜓))) | ||
Theorem | ibibr 370 | Implication in terms of implication and biconditional. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 21-Dec-2013.) |
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → (𝜓 ↔ 𝜑))) | ||
Theorem | tbt 371 | A wff is equivalent to its equivalence with a truth. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ 𝜑 ⇒ ⊢ (𝜓 ↔ (𝜓 ↔ 𝜑)) | ||
Theorem | nbn2 372 | The negation of a wff is equivalent to the wff's equivalence to falsehood. (Contributed by Juha Arpiainen, 19-Jan-2006.) (Proof shortened by Wolf Lammen, 28-Jan-2013.) |
⊢ (¬ 𝜑 → (¬ 𝜓 ↔ (𝜑 ↔ 𝜓))) | ||
Theorem | bibif 373 | Transfer negation via an equivalence. (Contributed by NM, 3-Oct-2007.) (Proof shortened by Wolf Lammen, 28-Jan-2013.) |
⊢ (¬ 𝜓 → ((𝜑 ↔ 𝜓) ↔ ¬ 𝜑)) | ||
Theorem | nbn 374 | The negation of a wff is equivalent to the wff's equivalence to falsehood. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 3-Oct-2013.) |
⊢ ¬ 𝜑 ⇒ ⊢ (¬ 𝜓 ↔ (𝜓 ↔ 𝜑)) | ||
Theorem | nbn3 375 | Transfer falsehood via equivalence. (Contributed by NM, 11-Sep-2006.) |
⊢ 𝜑 ⇒ ⊢ (¬ 𝜓 ↔ (𝜓 ↔ ¬ 𝜑)) | ||
Theorem | pm5.21im 376 | Two propositions are equivalent if they are both false. Closed form of 2false 377. Equivalent to a biimpr 221-like version of the xor-connective. (Contributed by Wolf Lammen, 13-May-2013.) |
⊢ (¬ 𝜑 → (¬ 𝜓 → (𝜑 ↔ 𝜓))) | ||
Theorem | 2false 377 | Two falsehoods are equivalent. (Contributed by NM, 4-Apr-2005.) (Proof shortened by Wolf Lammen, 19-May-2013.) |
⊢ ¬ 𝜑 & ⊢ ¬ 𝜓 ⇒ ⊢ (𝜑 ↔ 𝜓) | ||
Theorem | 2falsed 378 | Two falsehoods are equivalent (deduction form). (Contributed by NM, 11-Oct-2013.) |
⊢ (𝜑 → ¬ 𝜓) & ⊢ (𝜑 → ¬ 𝜒) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | pm5.21ni 379 | Two propositions implying a false one are equivalent. (Contributed by NM, 16-Feb-1996.) (Proof shortened by Wolf Lammen, 19-May-2013.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜓) ⇒ ⊢ (¬ 𝜓 → (𝜑 ↔ 𝜒)) | ||
Theorem | pm5.21nii 380 | Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 21-May-1999.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜓) & ⊢ (𝜓 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (𝜑 ↔ 𝜒) | ||
Theorem | pm5.21ndd 381 | Eliminate an antecedent implied by each side of a biconditional, deduction version. (Contributed by Paul Chapman, 21-Nov-2012.) (Proof shortened by Wolf Lammen, 6-Oct-2013.) |
⊢ (𝜑 → (𝜒 → 𝜓)) & ⊢ (𝜑 → (𝜃 → 𝜓)) & ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) ⇒ ⊢ (𝜑 → (𝜒 ↔ 𝜃)) | ||
Theorem | bija 382 | Combine antecedents into a single biconditional. This inference, reminiscent of ja 187, is reversible: The hypotheses can be deduced from the conclusion alone (see pm5.1im 264 and pm5.21im 376). (Contributed by Wolf Lammen, 13-May-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (¬ 𝜑 → (¬ 𝜓 → 𝜒)) ⇒ ⊢ ((𝜑 ↔ 𝜓) → 𝜒) | ||
Theorem | pm5.18 383 | Theorem *5.18 of [WhiteheadRussell] p. 124. This theorem says that logical equivalence is the same as negated "exclusive or". (Contributed by NM, 28-Jun-2002.) (Proof shortened by Andrew Salmon, 20-Jun-2011.) (Proof shortened by Wolf Lammen, 15-Oct-2013.) |
⊢ ((𝜑 ↔ 𝜓) ↔ ¬ (𝜑 ↔ ¬ 𝜓)) | ||
Theorem | xor3 384 | Two ways to express "exclusive or". (Contributed by NM, 1-Jan-2006.) |
⊢ (¬ (𝜑 ↔ 𝜓) ↔ (𝜑 ↔ ¬ 𝜓)) | ||
Theorem | nbbn 385 | Move negation outside of biconditional. Compare Theorem *5.18 of [WhiteheadRussell] p. 124. (Contributed by NM, 27-Jun-2002.) (Proof shortened by Wolf Lammen, 20-Sep-2013.) |
⊢ ((¬ 𝜑 ↔ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓)) | ||
Theorem | biass 386 | Associative law for the biconditional. An axiom of system DS in Vladimir Lifschitz, "On calculational proofs", Annals of Pure and Applied Logic, 113:207-224, 2002, http://www.cs.utexas.edu/users/ai-lab/pub-view.php?PubID=26805. Interestingly, this law was not included in Principia Mathematica but was apparently first noted by Jan Lukasiewicz circa 1923. (Contributed by NM, 8-Jan-2005.) (Proof shortened by Juha Arpiainen, 19-Jan-2006.) (Proof shortened by Wolf Lammen, 21-Sep-2013.) |
⊢ (((𝜑 ↔ 𝜓) ↔ 𝜒) ↔ (𝜑 ↔ (𝜓 ↔ 𝜒))) | ||
Theorem | biluk 387 | Lukasiewicz's shortest axiom for equivalential calculus. Storrs McCall, ed., Polish Logic 1920-1939 (Oxford, 1967), p. 96. (Contributed by NM, 10-Jan-2005.) |
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜒 ↔ 𝜓) ↔ (𝜑 ↔ 𝜒))) | ||
Theorem | pm5.19 388 | Theorem *5.19 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) |
⊢ ¬ (𝜑 ↔ ¬ 𝜑) | ||
Theorem | bi2.04 389 | Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 11-May-1993.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒))) | ||
Theorem | pm5.4 390 | Antecedent absorption implication. Theorem *5.4 of [WhiteheadRussell] p. 125. (Contributed by NM, 5-Aug-1993.) |
⊢ ((𝜑 → (𝜑 → 𝜓)) ↔ (𝜑 → 𝜓)) | ||
Theorem | imdi 391 | Distributive law for implication. Compare Theorem *5.41 of [WhiteheadRussell] p. 125. (Contributed by NM, 5-Aug-1993.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ ((𝜑 → 𝜓) → (𝜑 → 𝜒))) | ||
Theorem | pm5.41 392 | Theorem *5.41 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 12-Oct-2012.) |
⊢ (((𝜑 → 𝜓) → (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 → 𝜒))) | ||
Theorem | pm4.8 393 | Theorem *4.8 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → ¬ 𝜑) ↔ ¬ 𝜑) | ||
Theorem | pm4.81 394 | A formula is equivalent to its negation implying it. Theorem *4.81 of [WhiteheadRussell] p. 122. Note that the second step, using pm2.24 124, could also use ax-1 6. (Contributed by NM, 3-Jan-2005.) |
⊢ ((¬ 𝜑 → 𝜑) ↔ 𝜑) | ||
Theorem | imim21b 395 | Simplify an implication between two implications when the antecedent of the first is a consequence of the antecedent of the second. The reverse form is useful in producing the successor step in induction proofs. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Wolf Lammen, 14-Sep-2013.) |
⊢ ((𝜓 → 𝜑) → (((𝜑 → 𝜒) → (𝜓 → 𝜃)) ↔ (𝜓 → (𝜒 → 𝜃)))) | ||
This section defines conjunction of two formulas, denoted by infix "∧ " and read "and". It is defined in terms of implication and negation, which is possible in classical logic (but not in intuitionistic logic: see iset.mm). After the definition, we briefly introduce conversion of simple expressions to and from conjunction. Two simple operations called importation (imp 407) and exportation (ex 413) follow. In the propositions-as-types interpretation, they correspond to uncurrying and currying respectively. They are foundational for this section. Most of the theorems proved here trace back to them, mostly indirectly, in a layered fashion, where more complex expressions are built from simpler ones. Here are some of these successive layers: importation and exportation, commutativity and associativity laws, adding antecedents and simplifying, conjunction of consequents, syllogisms, etc. As indicated in the "note on definitions" in the section comment for logical equivalence, some theorems containing only implication, negation and conjunction are placed in the section after disjunction since theirs proofs use disjunction (although this is not required since definitions are conservative, see said section comment). | ||
Syntax | wa 396 | Extend wff definition to include conjunction ("and"). |
wff (𝜑 ∧ 𝜓) | ||
Definition | df-an 397 |
Define conjunction (logical "and"). Definition of [Margaris] p. 49. When
both the left and right operand are true, the result is true; when either
is false, the result is false. For example, it is true that
(2 = 2 ∧ 3 = 3). After we define the constant
true ⊤
(df-tru 1531) and the constant false ⊥ (df-fal 1541), we will be able
to prove these truth table values: ((⊤ ∧
⊤) ↔ ⊤)
(truantru 1561), ((⊤ ∧ ⊥)
↔ ⊥) (truanfal 1562),
((⊥ ∧ ⊤) ↔ ⊥) (falantru 1563), and
((⊥ ∧ ⊥) ↔ ⊥) (falanfal 1564).
This is our first use of the biconditional connective in a definition; we use the biconditional connective in place of the traditional "<=def=>", which means the same thing, except that we can manipulate the biconditional connective directly in proofs rather than having to rely on an informal definition substitution rule. Note that if we mechanically substitute ¬ (𝜑 → ¬ 𝜓) for (𝜑 ∧ 𝜓), we end up with an instance of previously proved theorem biid 262. This is the justification for the definition, along with the fact that it introduces a new symbol ∧. Contrast with ∨ (df-or 842), → (wi 4), ⊼ (df-nan 1476), and ⊻ (df-xor 1496). (Contributed by NM, 5-Jan-1993.) |
⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓)) | ||
Theorem | pm4.63 398 | Theorem *4.63 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (𝜑 → ¬ 𝜓) ↔ (𝜑 ∧ 𝜓)) | ||
Theorem | pm4.67 399 | Theorem *4.67 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (¬ 𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∧ 𝜓)) | ||
Theorem | imnan 400 | Express an implication in terms of a negated conjunction. (Contributed by NM, 9-Apr-1994.) |
⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |