Home | Metamath
Proof Explorer Theorem List (p. 4 of 450) | < 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-28694) |
Hilbert Space Explorer
(28695-30217) |
Users' Mathboxes
(30218-44905) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 3bitr2i 301 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ (𝜑 ↔ 𝜃) | ||
Theorem | 3bitr2ri 302 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ (𝜃 ↔ 𝜑) | ||
Theorem | 3bitr3i 303 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜑 ↔ 𝜒) & ⊢ (𝜓 ↔ 𝜃) ⇒ ⊢ (𝜒 ↔ 𝜃) | ||
Theorem | 3bitr3ri 304 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 21-Jun-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜑 ↔ 𝜒) & ⊢ (𝜓 ↔ 𝜃) ⇒ ⊢ (𝜃 ↔ 𝜒) | ||
Theorem | 3bitr4i 305 | 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 306 | A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜓) ⇒ ⊢ (𝜃 ↔ 𝜒) | ||
Theorem | 3bitrd 307 | Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜒 ↔ 𝜃)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜏)) | ||
Theorem | 3bitrrd 308 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜒 ↔ 𝜃)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜏 ↔ 𝜓)) | ||
Theorem | 3bitr2d 309 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜏)) | ||
Theorem | 3bitr2rd 310 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜏 ↔ 𝜓)) | ||
Theorem | 3bitr3d 311 | Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 24-Apr-1996.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜓 ↔ 𝜃)) & ⊢ (𝜑 → (𝜒 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | ||
Theorem | 3bitr3rd 312 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜓 ↔ 𝜃)) & ⊢ (𝜑 → (𝜒 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜏 ↔ 𝜃)) | ||
Theorem | 3bitr4d 313 | Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 18-Oct-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜓)) & ⊢ (𝜑 → (𝜏 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | ||
Theorem | 3bitr4rd 314 | Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜓)) & ⊢ (𝜑 → (𝜏 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜏 ↔ 𝜃)) | ||
Theorem | 3bitr3g 315 | More general version of 3bitr3i 303. Useful for converting definitions in a formula. (Contributed by NM, 4-Jun-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜓 ↔ 𝜃) & ⊢ (𝜒 ↔ 𝜏) ⇒ ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | ||
Theorem | 3bitr4g 316 | More general version of 3bitr4i 305. Useful for converting definitions in a formula. (Contributed by NM, 11-May-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 ↔ 𝜓) & ⊢ (𝜏 ↔ 𝜒) ⇒ ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | ||
Theorem | notnotb 317 | Double negation. Theorem *4.13 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 ↔ ¬ ¬ 𝜑) | ||
Theorem | con34b 318 | A biconditional form of contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116. (Contributed by NM, 11-May-1993.) |
⊢ ((𝜑 → 𝜓) ↔ (¬ 𝜓 → ¬ 𝜑)) | ||
Theorem | con4bid 319 | A contraposition deduction. (Contributed by NM, 21-May-1994.) |
⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | notbid 320 | Deduction negating both sides of a logical equivalence. (Contributed by NM, 21-May-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒)) | ||
Theorem | notbi 321 | Contraposition. Theorem *4.11 of [WhiteheadRussell] p. 117. (Contributed by NM, 21-May-1994.) (Proof shortened by Wolf Lammen, 12-Jun-2013.) |
⊢ ((𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓)) | ||
Theorem | notbii 322 | Negate both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (¬ 𝜑 ↔ ¬ 𝜓) | ||
Theorem | con4bii 323 | A contraposition inference. (Contributed by NM, 21-May-1994.) |
⊢ (¬ 𝜑 ↔ ¬ 𝜓) ⇒ ⊢ (𝜑 ↔ 𝜓) | ||
Theorem | mtbi 324 | 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 325 | 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 326 | A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.) |
⊢ (𝜑 → ¬ 𝜓) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜒) | ||
Theorem | mtbird 327 | A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 10-May-1994.) |
⊢ (𝜑 → ¬ 𝜒) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | mtbii 328 | An inference from a biconditional, similar to modus tollens. (Contributed by NM, 27-Nov-1995.) |
⊢ ¬ 𝜓 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜒) | ||
Theorem | mtbiri 329 | An inference from a biconditional, similar to modus tollens. (Contributed by NM, 24-Aug-1995.) |
⊢ ¬ 𝜒 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | sylnib 330 | A mixed syllogism inference from an implication and a biconditional. (Contributed by Wolf Lammen, 16-Dec-2013.) |
⊢ (𝜑 → ¬ 𝜓) & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (𝜑 → ¬ 𝜒) | ||
Theorem | sylnibr 331 | 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 332 | 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 333 | A mixed syllogism inference from a biconditional and an implication. (Contributed by Wolf Lammen, 16-Dec-2013.) |
⊢ (𝜓 ↔ 𝜑) & ⊢ (¬ 𝜓 → 𝜒) ⇒ ⊢ (¬ 𝜑 → 𝜒) | ||
Theorem | xchnxbi 334 | Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.) |
⊢ (¬ 𝜑 ↔ 𝜓) & ⊢ (𝜑 ↔ 𝜒) ⇒ ⊢ (¬ 𝜒 ↔ 𝜓) | ||
Theorem | xchnxbir 335 | Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.) |
⊢ (¬ 𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜑) ⇒ ⊢ (¬ 𝜒 ↔ 𝜓) | ||
Theorem | xchbinx 336 | Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.) |
⊢ (𝜑 ↔ ¬ 𝜓) & ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (𝜑 ↔ ¬ 𝜒) | ||
Theorem | xchbinxr 337 | Replacement of a subexpression by an equivalent one. (Contributed by Wolf Lammen, 27-Sep-2014.) |
⊢ (𝜑 ↔ ¬ 𝜓) & ⊢ (𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 ↔ ¬ 𝜒) | ||
Theorem | imbi2i 338 | 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 | jcndOLD 339 | Obsolete version of jcnd 165 as of 10-Apr-2024. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → ¬ 𝜒) ⇒ ⊢ (𝜑 → ¬ (𝜓 → 𝜒)) | ||
Theorem | bibi2i 340 | 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 341 | Inference adding a biconditional to the right in an equivalence. (Contributed by NM, 26-May-1993.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒)) | ||
Theorem | bibi12i 342 | The equivalence of two equivalences. (Contributed by NM, 26-May-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜃)) | ||
Theorem | imbi2d 343 | Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 → 𝜓) ↔ (𝜃 → 𝜒))) | ||
Theorem | imbi1d 344 | 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 345 | 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 346 | Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 11-May-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃))) | ||
Theorem | imbi12d 347 | Deduction joining two equivalences to form equivalence of implications. (Contributed by NM, 16-May-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏))) | ||
Theorem | bibi12d 348 | Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 26-May-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏))) | ||
Theorem | imbi12 349 | Closed form of imbi12i 353. 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 350 | Theorem *4.84 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))) | ||
Theorem | imbi2 351 | Theorem *4.85 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 19-May-2013.) |
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))) | ||
Theorem | imbi1i 352 | 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 353 | Join two logical equivalences to form equivalence of implications. (Contributed by NM, 1-Aug-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)) | ||
Theorem | bibi1 354 | Theorem *4.86 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒))) | ||
Theorem | bitr3 355 | Closed nested implication form of bitr3i 279. Derived automatically from bitr3VD 41181. (Contributed by Alan Sare, 31-Dec-2011.) |
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ↔ 𝜒) → (𝜓 ↔ 𝜒))) | ||
Theorem | con2bi 356 | Contraposition. Theorem *4.12 of [WhiteheadRussell] p. 117. (Contributed by NM, 15-Apr-1995.) (Proof shortened by Wolf Lammen, 3-Jan-2013.) |
⊢ ((𝜑 ↔ ¬ 𝜓) ↔ (𝜓 ↔ ¬ 𝜑)) | ||
Theorem | con2bid 357 | A contraposition deduction. (Contributed by NM, 15-Apr-1995.) |
⊢ (𝜑 → (𝜓 ↔ ¬ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 ↔ ¬ 𝜓)) | ||
Theorem | con1bid 358 | A contraposition deduction. (Contributed by NM, 9-Oct-1999.) |
⊢ (𝜑 → (¬ 𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (¬ 𝜒 ↔ 𝜓)) | ||
Theorem | con1bii 359 | A contraposition inference. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.) |
⊢ (¬ 𝜑 ↔ 𝜓) ⇒ ⊢ (¬ 𝜓 ↔ 𝜑) | ||
Theorem | con2bii 360 | A contraposition inference. (Contributed by NM, 12-Mar-1993.) |
⊢ (𝜑 ↔ ¬ 𝜓) ⇒ ⊢ (𝜓 ↔ ¬ 𝜑) | ||
Theorem | con1b 361 | Contraposition. Bidirectional version of con1 148. (Contributed by NM, 3-Jan-1993.) |
⊢ ((¬ 𝜑 → 𝜓) ↔ (¬ 𝜓 → 𝜑)) | ||
Theorem | con2b 362 | Contraposition. Bidirectional version of con2 137. (Contributed by NM, 12-Mar-1993.) |
⊢ ((𝜑 → ¬ 𝜓) ↔ (𝜓 → ¬ 𝜑)) | ||
Theorem | biimt 363 | A wff is equivalent to itself with true antecedent. (Contributed by NM, 28-Jan-1996.) |
⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓))) | ||
Theorem | pm5.5 364 | Theorem *5.5 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
⊢ (𝜑 → ((𝜑 → 𝜓) ↔ 𝜓)) | ||
Theorem | a1bi 365 | Inference introducing a theorem as an antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Nov-2012.) |
⊢ 𝜑 ⇒ ⊢ (𝜓 ↔ (𝜑 → 𝜓)) | ||
Theorem | mt2bi 366 | A false consequent falsifies an antecedent. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.) |
⊢ 𝜑 ⇒ ⊢ (¬ 𝜓 ↔ (𝜓 → ¬ 𝜑)) | ||
Theorem | mtt 367 | Modus-tollens-like theorem. (Contributed by NM, 7-Apr-2001.) (Proof shortened by Wolf Lammen, 12-Nov-2012.) |
⊢ (¬ 𝜑 → (¬ 𝜓 ↔ (𝜓 → 𝜑))) | ||
Theorem | imnot 368 | 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 364 (true antecedent). (Contributed by Mario Carneiro, 26-Apr-2019.) (Proof shortened by Wolf Lammen, 26-May-2019.) |
⊢ (¬ 𝜓 → ((𝜑 → 𝜓) ↔ ¬ 𝜑)) | ||
Theorem | pm5.501 369 | Theorem *5.501 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
⊢ (𝜑 → (𝜓 ↔ (𝜑 ↔ 𝜓))) | ||
Theorem | ibib 370 | Implication in terms of implication and biconditional. (Contributed by NM, 31-Mar-1994.) (Proof shortened by Wolf Lammen, 24-Jan-2013.) |
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → (𝜑 ↔ 𝜓))) | ||
Theorem | ibibr 371 | Implication in terms of implication and biconditional. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 21-Dec-2013.) |
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → (𝜓 ↔ 𝜑))) | ||
Theorem | tbt 372 | 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 373 | 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 374 | Transfer negation via an equivalence. (Contributed by NM, 3-Oct-2007.) (Proof shortened by Wolf Lammen, 28-Jan-2013.) |
⊢ (¬ 𝜓 → ((𝜑 ↔ 𝜓) ↔ ¬ 𝜑)) | ||
Theorem | nbn 375 | 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 376 | Transfer falsehood via equivalence. (Contributed by NM, 11-Sep-2006.) |
⊢ 𝜑 ⇒ ⊢ (¬ 𝜓 ↔ (𝜓 ↔ ¬ 𝜑)) | ||
Theorem | pm5.21im 377 | Two propositions are equivalent if they are both false. Closed form of 2false 378. Equivalent to a biimpr 222-like version of the xor-connective. (Contributed by Wolf Lammen, 13-May-2013.) |
⊢ (¬ 𝜑 → (¬ 𝜓 → (𝜑 ↔ 𝜓))) | ||
Theorem | 2false 378 | Two falsehoods are equivalent. (Contributed by NM, 4-Apr-2005.) (Proof shortened by Wolf Lammen, 19-May-2013.) |
⊢ ¬ 𝜑 & ⊢ ¬ 𝜓 ⇒ ⊢ (𝜑 ↔ 𝜓) | ||
Theorem | 2falsed 379 | Two falsehoods are equivalent (deduction form). (Contributed by NM, 11-Oct-2013.) (Proof shortened by Wolf Lammen, 11-Apr-2024.) |
⊢ (𝜑 → ¬ 𝜓) & ⊢ (𝜑 → ¬ 𝜒) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | 2falsedOLD 380 | Obsolete version of 2falsed 379 as of 11-Apr-2024. (Contributed by NM, 11-Oct-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ¬ 𝜓) & ⊢ (𝜑 → ¬ 𝜒) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | pm5.21ni 381 | 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 382 | Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 21-May-1999.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜓) & ⊢ (𝜓 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (𝜑 ↔ 𝜒) | ||
Theorem | pm5.21ndd 383 | 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 384 | Combine antecedents into a single biconditional. This inference, reminiscent of ja 188, is reversible: The hypotheses can be deduced from the conclusion alone (see pm5.1im 265 and pm5.21im 377). (Contributed by Wolf Lammen, 13-May-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (¬ 𝜑 → (¬ 𝜓 → 𝜒)) ⇒ ⊢ ((𝜑 ↔ 𝜓) → 𝜒) | ||
Theorem | pm5.18 385 | 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 386 | Two ways to express "exclusive or". (Contributed by NM, 1-Jan-2006.) |
⊢ (¬ (𝜑 ↔ 𝜓) ↔ (𝜑 ↔ ¬ 𝜓)) | ||
Theorem | nbbn 387 | 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 388 | 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 389 | 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 390 | Theorem *5.19 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) |
⊢ ¬ (𝜑 ↔ ¬ 𝜑) | ||
Theorem | bi2.04 391 | Logical equivalence of commuted antecedents. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 11-May-1993.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒))) | ||
Theorem | pm5.4 392 | Antecedent absorption implication. Theorem *5.4 of [WhiteheadRussell] p. 125. (Contributed by NM, 5-Aug-1993.) |
⊢ ((𝜑 → (𝜑 → 𝜓)) ↔ (𝜑 → 𝜓)) | ||
Theorem | imdi 393 | Distributive law for implication. Compare Theorem *5.41 of [WhiteheadRussell] p. 125. (Contributed by NM, 5-Aug-1993.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ ((𝜑 → 𝜓) → (𝜑 → 𝜒))) | ||
Theorem | pm5.41 394 | Theorem *5.41 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 12-Oct-2012.) |
⊢ (((𝜑 → 𝜓) → (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 → 𝜒))) | ||
Theorem | pm4.8 395 | Theorem *4.8 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → ¬ 𝜑) ↔ ¬ 𝜑) | ||
Theorem | pm4.81 396 | 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 397 | 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 409) and exportation (ex 415) 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 398 | Extend wff definition to include conjunction ("and"). |
wff (𝜑 ∧ 𝜓) | ||
Definition | df-an 399 |
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 1536) and the constant false ⊥ (df-fal 1546), we will be able
to prove these truth table values: ((⊤ ∧
⊤) ↔ ⊤)
(truantru 1566), ((⊤ ∧ ⊥)
↔ ⊥) (truanfal 1567),
((⊥ ∧ ⊤) ↔ ⊥) (falantru 1568), and
((⊥ ∧ ⊥) ↔ ⊥) (falanfal 1569).
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 263. This is the justification for the definition, along with the fact that it introduces a new symbol ∧. Contrast with ∨ (df-or 844), → (wi 4), ⊼ (df-nan 1481), and ⊻ (df-xor 1501). (Contributed by NM, 5-Jan-1993.) |
⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓)) | ||
Theorem | pm4.63 400 | Theorem *4.63 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (𝜑 → ¬ 𝜓) ↔ (𝜑 ∧ 𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |