Home | Metamath
Proof Explorer Theorem List (p. 15 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 3an6 1401 | Analogue of an4 861 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) ↔ ((𝜑 ∧ 𝜒 ∧ 𝜏) ∧ (𝜓 ∧ 𝜃 ∧ 𝜂))) | ||
Theorem | 3or6 1402 | Analogue of or4 549 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.) |
⊢ (((𝜑 ∨ 𝜓) ∨ (𝜒 ∨ 𝜃) ∨ (𝜏 ∨ 𝜂)) ↔ ((𝜑 ∨ 𝜒 ∨ 𝜏) ∨ (𝜓 ∨ 𝜃 ∨ 𝜂))) | ||
Theorem | mp3an1 1403 | An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
⊢ 𝜑 & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | mp3an2 1404 | An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | ||
Theorem | mp3an3 1405 | An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
⊢ 𝜒 & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜃) | ||
Theorem | mp3an12 1406 | An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜒 → 𝜃) | ||
Theorem | mp3an13 1407 | An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.) |
⊢ 𝜑 & ⊢ 𝜒 & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜓 → 𝜃) | ||
Theorem | mp3an23 1408 | An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.) |
⊢ 𝜓 & ⊢ 𝜒 & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | mp3an1i 1409 | An inference based on modus ponens. (Contributed by NM, 5-Jul-2005.) |
⊢ 𝜓 & ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) ⇒ ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜏)) | ||
Theorem | mp3anl1 1410 | An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.) |
⊢ 𝜑 & ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||
Theorem | mp3anl2 1411 | An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.) |
⊢ 𝜓 & ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||
Theorem | mp3anl3 1412 | An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.) |
⊢ 𝜒 & ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏) | ||
Theorem | mp3anr1 1413 | An inference based on modus ponens. (Contributed by NM, 4-Nov-2006.) |
⊢ 𝜓 & ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜃)) → 𝜏) | ||
Theorem | mp3anr2 1414 | An inference based on modus ponens. (Contributed by NM, 24-Nov-2006.) |
⊢ 𝜒 & ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜏) | ||
Theorem | mp3anr3 1415 | An inference based on modus ponens. (Contributed by NM, 19-Oct-2007.) |
⊢ 𝜃 & ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏) | ||
Theorem | mp3an 1416 | An inference based on modus ponens. (Contributed by NM, 14-May-1999.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ 𝜃 | ||
Theorem | mpd3an3 1417 | An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜃) | ||
Theorem | mpd3an23 1418 | An inference based on modus ponens. (Contributed by NM, 4-Dec-2006.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | mp3and 1419 | A deduction based on modus ponens. (Contributed by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) ⇒ ⊢ (𝜑 → 𝜏) | ||
Theorem | mp3an12i 1420 | mp3an 1416 with antecedents in standard conjunction form and with one hypothesis an implication. (Contributed by Alan Sare, 28-Aug-2016.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ (𝜒 → 𝜃) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜒 → 𝜏) | ||
Theorem | mp3an2i 1421 | mp3an 1416 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.) |
⊢ 𝜑 & ⊢ (𝜓 → 𝜒) & ⊢ (𝜓 → 𝜃) & ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜓 → 𝜏) | ||
Theorem | mp3an3an 1422 | mp3an 1416 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.) |
⊢ 𝜑 & ⊢ (𝜓 → 𝜒) & ⊢ (𝜃 → 𝜏) & ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜓 ∧ 𝜃) → 𝜂) | ||
Theorem | mp3an2ani 1423 | An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ 𝜑 & ⊢ (𝜓 → 𝜒) & ⊢ ((𝜓 ∧ 𝜃) → 𝜏) & ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜓 ∧ 𝜃) → 𝜂) | ||
Theorem | biimp3a 1424 | Infer implication from a logical equivalence. Similar to biimpa 500. (Contributed by NM, 4-Sep-2005.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | biimp3ar 1425 | Infer implication from a logical equivalence. Similar to biimpar 501. (Contributed by NM, 2-Jan-2009.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) | ||
Theorem | 3anandis 1426 | Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 18-Apr-2007.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒) ∧ (𝜑 ∧ 𝜃)) → 𝜏) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) | ||
Theorem | 3anandirs 1427 | Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 25-Jul-2006.) |
⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜃) ∧ (𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||
Theorem | ecase23d 1428 | Deduction for elimination by cases. (Contributed by NM, 22-Apr-1994.) |
⊢ (𝜑 → ¬ 𝜒) & ⊢ (𝜑 → ¬ 𝜃) & ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | 3ecase 1429 | Inference for elimination by cases. (Contributed by NM, 13-Jul-2005.) |
⊢ (¬ 𝜑 → 𝜃) & ⊢ (¬ 𝜓 → 𝜃) & ⊢ (¬ 𝜒 → 𝜃) & ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ 𝜃 | ||
Theorem | 3bior1fd 1430 | A disjunction is equivalent to a threefold disjunction with single falsehood, analogous to biorf 419. (Contributed by Alexander van der Vekens, 8-Sep-2017.) |
⊢ (𝜑 → ¬ 𝜃) ⇒ ⊢ (𝜑 → ((𝜒 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒 ∨ 𝜓))) | ||
Theorem | 3bior1fand 1431 | A disjunction is equivalent to a threefold disjunction with single falsehood of a conjunction. (Contributed by Alexander van der Vekens, 8-Sep-2017.) |
⊢ (𝜑 → ¬ 𝜃) ⇒ ⊢ (𝜑 → ((𝜒 ∨ 𝜓) ↔ ((𝜃 ∧ 𝜏) ∨ 𝜒 ∨ 𝜓))) | ||
Theorem | 3bior2fd 1432 | A wff is equivalent to its threefold disjunction with double falsehood, analogous to biorf 419. (Contributed by Alexander van der Vekens, 8-Sep-2017.) |
⊢ (𝜑 → ¬ 𝜃) & ⊢ (𝜑 → ¬ 𝜒) ⇒ ⊢ (𝜑 → (𝜓 ↔ (𝜃 ∨ 𝜒 ∨ 𝜓))) | ||
Theorem | 3biant1d 1433 | A conjunction is equivalent to a threefold conjunction with single truth, analogous to biantrud 527. (Contributed by Alexander van der Vekens, 26-Sep-2017.) |
⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜃 ∧ 𝜒 ∧ 𝜓))) | ||
Theorem | intn3an1d 1434 | Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | intn3an2d 1435 | Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓 ∧ 𝜃)) | ||
Theorem | intn3an3d 1436 | Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜃 ∧ 𝜓)) | ||
Theorem | an3andi 1437 | Distribution of conjunction over threefold conjunction. (Contributed by Thierry Arnoux, 8-Apr-2019.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒) ∧ (𝜑 ∧ 𝜃))) | ||
Theorem | an33rean 1438 | Rearrange a 9-fold conjunction. (Contributed by Thierry Arnoux, 14-Apr-2019.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) ↔ ((𝜑 ∧ 𝜏 ∧ 𝜌) ∧ ((𝜓 ∧ 𝜃) ∧ (𝜂 ∧ 𝜎) ∧ (𝜒 ∧ 𝜁)))) | ||
Syntax | wnan 1439 | Extend wff definition to include alternative denial ('nand'). |
wff (𝜑 ⊼ 𝜓) | ||
Definition | df-nan 1440 | Define incompatibility, or alternative denial ('not-and' or 'nand'). This is also called the Sheffer stroke, represented by a vertical bar, but we use a different symbol to avoid ambiguity with other uses of the vertical bar. In the second edition of Principia Mathematica (1927), Russell and Whitehead used the Sheffer stroke and suggested it as a replacement for the "or" and "not" operations of the first edition. However, in practice, "or" and "not" are more widely used. After we define the constant true ⊤ (df-tru 1478) and the constant false ⊥ (df-fal 1481), we will be able to prove these truth table values: ((⊤ ⊼ ⊤) ↔ ⊥) (trunantru 1515), ((⊤ ⊼ ⊥) ↔ ⊤) (trunanfal 1516), ((⊥ ⊼ ⊤) ↔ ⊤) (falnantru 1517), and ((⊥ ⊼ ⊥) ↔ ⊤) (falnanfal 1518). Contrast with ∧ (df-an 385), ∨ (df-or 384), → (wi 4), and ⊻ (df-xor 1457) . (Contributed by Jeff Hoffman, 19-Nov-2007.) |
⊢ ((𝜑 ⊼ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓)) | ||
Theorem | nanan 1441 | Write 'and' in terms of 'nand'. (Contributed by Mario Carneiro, 9-May-2015.) |
⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 ⊼ 𝜓)) | ||
Theorem | nancom 1442 | The 'nand' operator commutes. (Contributed by Mario Carneiro, 9-May-2015.) (Proof shortened by Wolf Lammen, 7-Mar-2020.) |
⊢ ((𝜑 ⊼ 𝜓) ↔ (𝜓 ⊼ 𝜑)) | ||
Theorem | nannan 1443 | Lemma for handling nested 'nand's. (Contributed by Jeff Hoffman, 19-Nov-2007.) (Proof shortened by Wolf Lammen, 7-Mar-2020.) |
⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ↔ (𝜑 → (𝜒 ∧ 𝜓))) | ||
Theorem | nanim 1444 | Show equivalence between implication and the Nicod version. To derive nic-dfim 1585, apply nanbi 1446. (Contributed by Jeff Hoffman, 19-Nov-2007.) |
⊢ ((𝜑 → 𝜓) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜓))) | ||
Theorem | nannot 1445 | Show equivalence between negation and the Nicod version. To derive nic-dfneg 1586, apply nanbi 1446. (Contributed by Jeff Hoffman, 19-Nov-2007.) |
⊢ (¬ 𝜓 ↔ (𝜓 ⊼ 𝜓)) | ||
Theorem | nanbi 1446 | Show equivalence between the biconditional and the Nicod version. (Contributed by Jeff Hoffman, 19-Nov-2007.) (Proof shortened by Wolf Lammen, 27-Jun-2020.) |
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜑) ⊼ (𝜓 ⊼ 𝜓)))) | ||
Theorem | nanbi1 1447 | Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.) |
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ⊼ 𝜒) ↔ (𝜓 ⊼ 𝜒))) | ||
Theorem | nanbi2 1448 | Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.) |
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ⊼ 𝜑) ↔ (𝜒 ⊼ 𝜓))) | ||
Theorem | nanbi12 1449 | Join two logical equivalences with anti-conjunction. (Contributed by SF, 2-Jan-2018.) |
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃)) → ((𝜑 ⊼ 𝜒) ↔ (𝜓 ⊼ 𝜃))) | ||
Theorem | nanbi1i 1450 | Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜑 ⊼ 𝜒) ↔ (𝜓 ⊼ 𝜒)) | ||
Theorem | nanbi2i 1451 | Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 ⊼ 𝜑) ↔ (𝜒 ⊼ 𝜓)) | ||
Theorem | nanbi12i 1452 | Join two logical equivalences with anti-conjunction. (Contributed by SF, 2-Jan-2018.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ ((𝜑 ⊼ 𝜒) ↔ (𝜓 ⊼ 𝜃)) | ||
Theorem | nanbi1d 1453 | Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 ⊼ 𝜃) ↔ (𝜒 ⊼ 𝜃))) | ||
Theorem | nanbi2d 1454 | Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 ⊼ 𝜓) ↔ (𝜃 ⊼ 𝜒))) | ||
Theorem | nanbi12d 1455 | Join two logical equivalences with anti-conjunction. (Contributed by Scott Fenton, 2-Jan-2018.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 ⊼ 𝜃) ↔ (𝜒 ⊼ 𝜏))) | ||
Syntax | wxo 1456 | Extend wff definition to include exclusive disjunction ('xor'). |
wff (𝜑 ⊻ 𝜓) | ||
Definition | df-xor 1457 | Define exclusive disjunction (logical 'xor'). Return true if either the left or right, but not both, are true. After we define the constant true ⊤ (df-tru 1478) and the constant false ⊥ (df-fal 1481), we will be able to prove these truth table values: ((⊤ ⊻ ⊤) ↔ ⊥) (truxortru 1519), ((⊤ ⊻ ⊥) ↔ ⊤) (truxorfal 1520), ((⊥ ⊻ ⊤) ↔ ⊤) (falxortru 1521), and ((⊥ ⊻ ⊥) ↔ ⊥) (falxorfal 1522). Contrast with ∧ (df-an 385), ∨ (df-or 384), → (wi 4), and ⊼ (df-nan 1440) . (Contributed by FL, 22-Nov-2010.) |
⊢ ((𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ↔ 𝜓)) | ||
Theorem | xnor 1458 | Two ways to write XNOR. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ ((𝜑 ↔ 𝜓) ↔ ¬ (𝜑 ⊻ 𝜓)) | ||
Theorem | xorcom 1459 | The connector ⊻ is commutative. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ ((𝜑 ⊻ 𝜓) ↔ (𝜓 ⊻ 𝜑)) | ||
Theorem | xorass 1460 | The connector ⊻ is associative. (Contributed by FL, 22-Nov-2010.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) (Proof shortened by Wolf Lammen, 20-Jun-2020.) |
⊢ (((𝜑 ⊻ 𝜓) ⊻ 𝜒) ↔ (𝜑 ⊻ (𝜓 ⊻ 𝜒))) | ||
Theorem | excxor 1461 | This tautology shows that xor is really exclusive. (Contributed by FL, 22-Nov-2010.) |
⊢ ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∧ ¬ 𝜓) ∨ (¬ 𝜑 ∧ 𝜓))) | ||
Theorem | xor2 1462 | Two ways to express "exclusive or." (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ ((𝜑 ⊻ 𝜓) ↔ ((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓))) | ||
Theorem | xoror 1463 | XOR implies OR. (Contributed by BJ, 19-Apr-2019.) |
⊢ ((𝜑 ⊻ 𝜓) → (𝜑 ∨ 𝜓)) | ||
Theorem | xornan 1464 | XOR implies NAND. (Contributed by BJ, 19-Apr-2019.) |
⊢ ((𝜑 ⊻ 𝜓) → ¬ (𝜑 ∧ 𝜓)) | ||
Theorem | xornan2 1465 | XOR implies NAND (written with the ⊼ connector). (Contributed by BJ, 19-Apr-2019.) |
⊢ ((𝜑 ⊻ 𝜓) → (𝜑 ⊼ 𝜓)) | ||
Theorem | xorneg2 1466 | The connector ⊻ is negated under negation of one argument. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 27-Jun-2020.) |
⊢ ((𝜑 ⊻ ¬ 𝜓) ↔ ¬ (𝜑 ⊻ 𝜓)) | ||
Theorem | xorneg1 1467 | The connector ⊻ is negated under negation of one argument. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 27-Jun-2020.) |
⊢ ((¬ 𝜑 ⊻ 𝜓) ↔ ¬ (𝜑 ⊻ 𝜓)) | ||
Theorem | xorneg 1468 | The connector ⊻ is unchanged under negation of both arguments. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ ((¬ 𝜑 ⊻ ¬ 𝜓) ↔ (𝜑 ⊻ 𝜓)) | ||
Theorem | xorbi12i 1469 | Equality property for XOR. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ ((𝜑 ⊻ 𝜒) ↔ (𝜓 ⊻ 𝜃)) | ||
Theorem | xorbi12d 1470 | Equality property for XOR. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 ⊻ 𝜃) ↔ (𝜒 ⊻ 𝜏))) | ||
Theorem | anxordi 1471 | Conjunction distributes over exclusive-or. In intuitionistic logic this assertion is also true, even though xordi 935 does not necessarily hold, in part because the usual definition of xor is subtly different in intuitionistic logic. (Contributed by David A. Wheeler, 7-Oct-2018.) |
⊢ ((𝜑 ∧ (𝜓 ⊻ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ⊻ (𝜑 ∧ 𝜒))) | ||
Theorem | xorexmid 1472 | Exclusive-or variant of the law of the excluded middle (exmid 430). This statement is ancient, going back to at least Stoic logic. This statement does not necessarily hold in intuitionistic logic. (Contributed by David A. Wheeler, 23-Feb-2019.) |
⊢ (𝜑 ⊻ ¬ 𝜑) | ||
Even though it isn't ordinarily part of propositional calculus, the universal quantifier ∀ is introduced here so that the soundness of definition df-tru 1478 can be checked by the same algorithm that is used for predicate calculus. Its first real use is in definition df-ex 1696 in the predicate calculus section below. For those who want propositional calculus to be self-contained i.e. to use wff variables only, the alternate definition dftru2 1483 may be adopted and this subsection moved down to the start of the subsection with wex 1695 below. However, the use of dftru2 1483 as a definition requires a more elaborate definition checking algorithm that we prefer to avoid. | ||
Syntax | wal 1473 | Extend wff definition to include the universal quantifier ('for all'). ∀𝑥𝜑 is read "𝜑 (phi) is true for all 𝑥." Typically, in its final application 𝜑 would be replaced with a wff containing a (free) occurrence of the variable 𝑥, for example 𝑥 = 𝑦. In a universe with a finite number of objects, "for all" is equivalent to a big conjunction (AND) with one wff for each possible case of 𝑥. When the universe is infinite (as with set theory), such a propositional-calculus equivalent is not possible because an infinitely long formula has no meaning, but conceptually the idea is the same. |
wff ∀𝑥𝜑 | ||
Even though it isn't ordinarily part of propositional calculus, the equality predicate = is introduced here so that the soundness of definition df-tru 1478 can be checked by the same algorithm as is used for predicate calculus. Its first real use is in theorem equs3 1862 in the predicate calculus section below. For those who want propositional calculus to be self-contained i.e. to use wff variables only, the alternate definition dftru2 1483 may be adopted and this subsection moved down to just above weq 1861 below. However, the use of dftru2 1483 as a definition requires a more elaborate definition checking algorithm that we prefer to avoid. | ||
Syntax | cv 1474 |
This syntax construction states that a variable 𝑥, which has been
declared to be a setvar variable by $f statement vx, is also a class
expression. This can be justified informally as follows. We know that
the class builder {𝑦 ∣ 𝑦 ∈ 𝑥} is a class by cab 2596.
Since (when
𝑦 is distinct from 𝑥) we
have 𝑥 =
{𝑦 ∣ 𝑦 ∈ 𝑥} by
cvjust 2605, we can argue that the syntax "class 𝑥 " can be viewed as
an abbreviation for "class {𝑦 ∣ 𝑦 ∈ 𝑥}". See the discussion
under the definition of class in [Jech] p.
4 showing that "Every set can
be considered to be a class."
While it is tempting and perhaps occasionally useful to view cv 1474 as a "type conversion" from a setvar variable to a class variable, keep in mind that cv 1474 is intrinsically no different from any other class-building syntax such as cab 2596, cun 3538, or c0 3874. For a general discussion of the theory of classes and the role of cv 1474, see mmset.html#class. (The description above applies to set theory, not predicate calculus. The purpose of introducing class 𝑥 here, and not in set theory where it belongs, is to allow us to express i.e. "prove" the weq 1861 of predicate calculus from the wceq 1475 of set theory, so that we don't overload the = connective with two syntax definitions. This is done to prevent ambiguity that would complicate some Metamath parsers.) |
class 𝑥 | ||
Syntax | wceq 1475 |
Extend wff definition to include class equality.
For a general discussion of the theory of classes, see mmset.html#class. (The purpose of introducing wff 𝐴 = 𝐵 here, and not in set theory where it belongs, is to allow us to express i.e. "prove" the weq 1861 of predicate calculus in terms of the wceq 1475 of set theory, so that we don't "overload" the = connective with two syntax definitions. This is done to prevent ambiguity that would complicate some Metamath parsers. For example, some parsers - although not the Metamath program - stumble on the fact that the = in 𝑥 = 𝑦 could be the = of either weq 1861 or wceq 1475, although mathematically it makes no difference. The class variables 𝐴 and 𝐵 are introduced temporarily for the purpose of this definition but otherwise not used in predicate calculus. See df-cleq 2603 for more information on the set theory usage of wceq 1475.) |
wff 𝐴 = 𝐵 | ||
Syntax | wtru 1476 | The constant ⊤ is a wff. |
wff ⊤ | ||
Theorem | trujust 1477 | Soundness justification theorem for df-tru 1478. (Contributed by Mario Carneiro, 17-Nov-2013.) (Revised by NM, 11-Jul-2019.) |
⊢ ((∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥) ↔ (∀𝑦 𝑦 = 𝑦 → ∀𝑦 𝑦 = 𝑦)) | ||
Definition | df-tru 1478 | Definition of the truth value "true", or "verum", denoted by ⊤. This is a tautology, as proved by tru 1479. In this definition, an instance of id 22 is used as the definiens, although any tautology, such as an axiom, can be used in its place. This particular id 22 instance was chosen so this definition can be checked by the same algorithm that is used for predicate calculus. This definition should be referenced directly only by tru 1479, and other proofs should depend on tru 1479 (directly or indirectly) instead of this definition, since there are many alternative ways to define ⊤. (Contributed by Anthony Hart, 13-Oct-2010.) (Revised by NM, 11-Jul-2019.) (New usage is discouraged.) |
⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)) | ||
Theorem | tru 1479 | The truth value ⊤ is provable. (Contributed by Anthony Hart, 13-Oct-2010.) |
⊢ ⊤ | ||
Syntax | wfal 1480 | The constant ⊥ is a wff. |
wff ⊥ | ||
Definition | df-fal 1481 | Definition of the truth value "false", or "falsum", denoted by ⊥. See also df-tru 1478. (Contributed by Anthony Hart, 22-Oct-2010.) |
⊢ (⊥ ↔ ¬ ⊤) | ||
Theorem | fal 1482 | The truth value ⊥ is refutable. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Mel L. O'Cat, 11-Mar-2012.) |
⊢ ¬ ⊥ | ||
Theorem | dftru2 1483 | An alternate definition of "true". (Contributed by Anthony Hart, 13-Oct-2010.) (Revised by BJ, 12-Jul-2019.) (New usage is discouraged.) |
⊢ (⊤ ↔ (𝜑 → 𝜑)) | ||
Theorem | trud 1484 | Eliminate ⊤ as an antecedent. A proposition implied by ⊤ is true. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ (⊤ → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | tbtru 1485 | A proposition is equivalent to itself being equivalent to ⊤. (Contributed by Anthony Hart, 14-Aug-2011.) |
⊢ (𝜑 ↔ (𝜑 ↔ ⊤)) | ||
Theorem | nbfal 1486 | The negation of a proposition is equivalent to itself being equivalent to ⊥. (Contributed by Anthony Hart, 14-Aug-2011.) |
⊢ (¬ 𝜑 ↔ (𝜑 ↔ ⊥)) | ||
Theorem | bitru 1487 | A theorem is equivalent to truth. (Contributed by Mario Carneiro, 9-May-2015.) |
⊢ 𝜑 ⇒ ⊢ (𝜑 ↔ ⊤) | ||
Theorem | bifal 1488 | A contradiction is equivalent to falsehood. (Contributed by Mario Carneiro, 9-May-2015.) |
⊢ ¬ 𝜑 ⇒ ⊢ (𝜑 ↔ ⊥) | ||
Theorem | falim 1489 | The truth value ⊥ implies anything. Also called the "principle of explosion", or "ex falso [sequitur]] quodlibet" (Latin for "from falsehood, anything [follows]]"). (Contributed by FL, 20-Mar-2011.) (Proof shortened by Anthony Hart, 1-Aug-2011.) |
⊢ (⊥ → 𝜑) | ||
Theorem | falimd 1490 | The truth value ⊥ implies anything. (Contributed by Mario Carneiro, 9-Feb-2017.) |
⊢ ((𝜑 ∧ ⊥) → 𝜓) | ||
Theorem | a1tru 1491 | Anything implies ⊤. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Anthony Hart, 1-Aug-2011.) |
⊢ (𝜑 → ⊤) | ||
Theorem | truan 1492 | True can be removed from a conjunction. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Wolf Lammen, 21-Jul-2019.) |
⊢ ((⊤ ∧ 𝜑) ↔ 𝜑) | ||
Theorem | dfnot 1493 | Given falsum ⊥, we can define the negation of a wff 𝜑 as the statement that ⊥ follows from assuming 𝜑. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 21-Jul-2019.) |
⊢ (¬ 𝜑 ↔ (𝜑 → ⊥)) | ||
Theorem | inegd 1494 | Negation introduction rule from natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.) |
⊢ ((𝜑 ∧ 𝜓) → ⊥) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | efald 1495 | Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.) |
⊢ ((𝜑 ∧ ¬ 𝜓) → ⊥) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | pm2.21fal 1496 | If a wff and its negation are provable, then falsum is provable. (Contributed by Mario Carneiro, 9-Feb-2017.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ⊥) | ||
Some sources define operations on true/false values using truth tables. These tables show the results of their operations for all possible combinations of true (⊤) and false (⊥). Here we show that our definitions and axioms produce equivalent results for ∧ (conjunction aka logical 'and') df-an 385, ∨ (disjunction aka logical inclusive 'or') df-or 384, → (implies) wi 4, ¬ (not) wn 3, ↔ (logical equivalence) df-bi 196, ⊼ (nand aka Sheffer stroke) df-nan 1440, and ⊻ (exclusive or) df-xor 1457. | ||
Theorem | truantru 1497 | A ∧ identity. (Contributed by Anthony Hart, 22-Oct-2010.) |
⊢ ((⊤ ∧ ⊤) ↔ ⊤) | ||
Theorem | truanfal 1498 | A ∧ identity. (Contributed by Anthony Hart, 22-Oct-2010.) |
⊢ ((⊤ ∧ ⊥) ↔ ⊥) | ||
Theorem | falantru 1499 | A ∧ identity. (Contributed by Anthony Hart, 22-Oct-2010.) |
⊢ ((⊥ ∧ ⊤) ↔ ⊥) | ||
Theorem | falanfal 1500 | A ∧ identity. (Contributed by Anthony Hart, 22-Oct-2010.) |
⊢ ((⊥ ∧ ⊥) ↔ ⊥) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |