Home | Metamath
Proof Explorer Theorem List (p. 15 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 3anbi13d 1401 | Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.) |
Theorem | 3anbi23d 1402 | Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.) |
Theorem | 3anbi1d 1403 | Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.) |
Theorem | 3anbi2d 1404 | Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.) |
Theorem | 3anbi3d 1405 | Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.) |
Theorem | 3anim123d 1406 | Deduction joining 3 implications to form implication of conjunctions. (Contributed by NM, 24-Feb-2005.) |
Theorem | 3orim123d 1407 | Deduction joining 3 implications to form implication of disjunctions. (Contributed by NM, 4-Apr-1997.) |
Theorem | an6 1408 | Rearrangement of 6 conjuncts. (Contributed by NM, 13-Mar-1995.) |
Theorem | 3an6 1409 | Analogue of an4 865 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Theorem | 3or6 1410 | Analogue of or4 550 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.) |
Theorem | mp3an1 1411 | An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
Theorem | mp3an2 1412 | An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
Theorem | mp3an3 1413 | An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
Theorem | mp3an12 1414 | An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.) |
Theorem | mp3an13 1415 | An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.) |
Theorem | mp3an23 1416 | An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.) |
Theorem | mp3an1i 1417 | An inference based on modus ponens. (Contributed by NM, 5-Jul-2005.) |
Theorem | mp3anl1 1418 | An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.) |
Theorem | mp3anl2 1419 | An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.) |
Theorem | mp3anl3 1420 | An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.) |
Theorem | mp3anr1 1421 | An inference based on modus ponens. (Contributed by NM, 4-Nov-2006.) |
Theorem | mp3anr2 1422 | An inference based on modus ponens. (Contributed by NM, 24-Nov-2006.) |
Theorem | mp3anr3 1423 | An inference based on modus ponens. (Contributed by NM, 19-Oct-2007.) |
Theorem | mp3an 1424 | An inference based on modus ponens. (Contributed by NM, 14-May-1999.) |
Theorem | mpd3an3 1425 | An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.) |
Theorem | mpd3an23 1426 | An inference based on modus ponens. (Contributed by NM, 4-Dec-2006.) |
Theorem | mp3and 1427 | A deduction based on modus ponens. (Contributed by Mario Carneiro, 24-Dec-2016.) |
Theorem | mp3an12i 1428 | mp3an 1424 with antecedents in standard conjunction form and with one hypothesis an implication. (Contributed by Alan Sare, 28-Aug-2016.) |
Theorem | mp3an2i 1429 | mp3an 1424 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.) |
Theorem | mp3an3an 1430 | mp3an 1424 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.) |
Theorem | mp3an2ani 1431 | An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.) |
Theorem | biimp3a 1432 | Infer implication from a logical equivalence. Similar to biimpa 501. (Contributed by NM, 4-Sep-2005.) |
Theorem | biimp3ar 1433 | Infer implication from a logical equivalence. Similar to biimpar 502. (Contributed by NM, 2-Jan-2009.) |
Theorem | 3anandis 1434 | Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 18-Apr-2007.) |
Theorem | 3anandirs 1435 | Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 25-Jul-2006.) |
Theorem | ecase23d 1436 | Deduction for elimination by cases. (Contributed by NM, 22-Apr-1994.) |
Theorem | 3ecase 1437 | Inference for elimination by cases. (Contributed by NM, 13-Jul-2005.) |
Theorem | 3bior1fd 1438 | A disjunction is equivalent to a threefold disjunction with single falsehood, analogous to biorf 420. (Contributed by Alexander van der Vekens, 8-Sep-2017.) |
Theorem | 3bior1fand 1439 | 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 1440 | A wff is equivalent to its threefold disjunction with double falsehood, analogous to biorf 420. (Contributed by Alexander van der Vekens, 8-Sep-2017.) |
Theorem | 3biant1d 1441 | A conjunction is equivalent to a threefold conjunction with single truth, analogous to biantrud 528. (Contributed by Alexander van der Vekens, 26-Sep-2017.) |
Theorem | intn3an1d 1442 | Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | intn3an2d 1443 | Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | intn3an3d 1444 | Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | an3andi 1445 | Distribution of conjunction over threefold conjunction. (Contributed by Thierry Arnoux, 8-Apr-2019.) |
Theorem | an33rean 1446 | Rearrange a 9-fold conjunction. (Contributed by Thierry Arnoux, 14-Apr-2019.) |
Syntax | wnan 1447 | Extend wff definition to include alternative denial ('nand'). |
Definition | df-nan 1448 | 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 1486) and the constant false (df-fal 1489), we will be able to prove these truth table values: (trunantru 1524), (trunanfal 1525), (falnantru 1526), and (falnanfal 1527). Contrast with (df-an 386), (df-or 385), (wi 4), and (df-xor 1465) . (Contributed by Jeff Hoffman, 19-Nov-2007.) |
Theorem | nanan 1449 | Write 'and' in terms of 'nand'. (Contributed by Mario Carneiro, 9-May-2015.) |
Theorem | nancom 1450 | The 'nand' operator commutes. (Contributed by Mario Carneiro, 9-May-2015.) (Proof shortened by Wolf Lammen, 7-Mar-2020.) |
Theorem | nannan 1451 | Lemma for handling nested 'nand's. (Contributed by Jeff Hoffman, 19-Nov-2007.) (Proof shortened by Wolf Lammen, 7-Mar-2020.) |
Theorem | nanim 1452 | Show equivalence between implication and the Nicod version. To derive nic-dfim 1594, apply nanbi 1454. (Contributed by Jeff Hoffman, 19-Nov-2007.) |
Theorem | nannot 1453 | Show equivalence between negation and the Nicod version. To derive nic-dfneg 1595, apply nanbi 1454. (Contributed by Jeff Hoffman, 19-Nov-2007.) |
Theorem | nanbi 1454 | 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 1455 | Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.) |
Theorem | nanbi2 1456 | Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.) |
Theorem | nanbi12 1457 | Join two logical equivalences with anti-conjunction. (Contributed by SF, 2-Jan-2018.) |
Theorem | nanbi1i 1458 | Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.) |
Theorem | nanbi2i 1459 | Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.) |
Theorem | nanbi12i 1460 | Join two logical equivalences with anti-conjunction. (Contributed by SF, 2-Jan-2018.) |
Theorem | nanbi1d 1461 | Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.) |
Theorem | nanbi2d 1462 | Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.) |
Theorem | nanbi12d 1463 | Join two logical equivalences with anti-conjunction. (Contributed by Scott Fenton, 2-Jan-2018.) |
Syntax | wxo 1464 | Extend wff definition to include exclusive disjunction ('xor'). |
Definition | df-xor 1465 | 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 1486) and the constant false (df-fal 1489), we will be able to prove these truth table values: (truxortru 1528), (truxorfal 1529), (falxortru 1530), and (falxorfal 1531). Contrast with (df-an 386), (df-or 385), (wi 4), and (df-nan 1448) . (Contributed by FL, 22-Nov-2010.) |
Theorem | xnor 1466 | Two ways to write XNOR. (Contributed by Mario Carneiro, 4-Sep-2016.) |
Theorem | xorcom 1467 | The connector is commutative. (Contributed by Mario Carneiro, 4-Sep-2016.) |
Theorem | xorass 1468 | 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 1469 | This tautology shows that xor is really exclusive. (Contributed by FL, 22-Nov-2010.) |
Theorem | xor2 1470 | Two ways to express "exclusive or." (Contributed by Mario Carneiro, 4-Sep-2016.) |
Theorem | xoror 1471 | XOR implies OR. (Contributed by BJ, 19-Apr-2019.) |
Theorem | xornan 1472 | XOR implies NAND. (Contributed by BJ, 19-Apr-2019.) |
Theorem | xornan2 1473 | XOR implies NAND (written with the connector). (Contributed by BJ, 19-Apr-2019.) |
Theorem | xorneg2 1474 | 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 1475 | 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 1476 | The connector is unchanged under negation of both arguments. (Contributed by Mario Carneiro, 4-Sep-2016.) |
Theorem | xorbi12i 1477 | Equality property for XOR. (Contributed by Mario Carneiro, 4-Sep-2016.) |
Theorem | xorbi12d 1478 | Equality property for XOR. (Contributed by Mario Carneiro, 4-Sep-2016.) |
Theorem | anxordi 1479 | Conjunction distributes over exclusive-or. In intuitionistic logic this assertion is also true, even though xordi 937 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 1480 | Exclusive-or variant of the law of the excluded middle (exmid 431). 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 1486 can be checked by the same algorithm that is used for predicate calculus. Its first real use is in definition df-ex 1705 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 1491 may be adopted and this subsection moved down to the start of the subsection with wex 1704 below. However, the use of dftru2 1491 as a definition requires a more elaborate definition checking algorithm that we prefer to avoid. | ||
Syntax | wal 1481 | 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. |
Even though it isn't ordinarily part of propositional calculus, the equality predicate is introduced here so that the soundness of definition df-tru 1486 can be checked by the same algorithm as is used for predicate calculus. Its first real use is in theorem equs3 1875 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 1491 may be adopted and this subsection moved down to just above weq 1874 below. However, the use of dftru2 1491 as a definition requires a more elaborate definition checking algorithm that we prefer to avoid. | ||
Syntax | cv 1482 |
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 2608.
Since (when
is distinct from
) we have by
cvjust 2617, we can argue that the syntax " " can be viewed as
an abbreviation for " ". 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 1482 as a "type conversion" from a setvar variable to a class variable, keep in mind that cv 1482 is intrinsically no different from any other class-building syntax such as cab 2608, cun 3572, or c0 3915. For a general discussion of the theory of classes and the role of cv 1482, see mmset.html#class. (The description above applies to set theory, not predicate calculus. The purpose of introducing here, and not in set theory where it belongs, is to allow us to express i.e. "prove" the weq 1874 of predicate calculus from the wceq 1483 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.) |
Syntax | wceq 1483 |
Extend wff definition to include class equality.
For a general discussion of the theory of classes, see mmset.html#class. (The purpose of introducing here, and not in set theory where it belongs, is to allow us to express i.e. "prove" the weq 1874 of predicate calculus in terms of the wceq 1483 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 1874 or wceq 1483, 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 2615 for more information on the set theory usage of wceq 1483.) |
Syntax | wtru 1484 | The constant is a wff. |
Theorem | trujust 1485 | Soundness justification theorem for df-tru 1486. (Contributed by Mario Carneiro, 17-Nov-2013.) (Revised by NM, 11-Jul-2019.) |
Definition | df-tru 1486 | Definition of the truth value "true", or "verum", denoted by . This is a tautology, as proved by tru 1487. 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 1487, and other proofs should depend on tru 1487 (directly or indirectly) instead of this definition, since there are many alternate ways to define . (Contributed by Anthony Hart, 13-Oct-2010.) (Revised by NM, 11-Jul-2019.) Use tru 1487 instead. (New usage is discouraged.) |
Theorem | tru 1487 | The truth value is provable. (Contributed by Anthony Hart, 13-Oct-2010.) |
Syntax | wfal 1488 | The constant is a wff. |
Definition | df-fal 1489 | Definition of the truth value "false", or "falsum", denoted by . See also df-tru 1486. (Contributed by Anthony Hart, 22-Oct-2010.) |
Theorem | fal 1490 | The truth value is refutable. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Mel L. O'Cat, 11-Mar-2012.) |
Theorem | dftru2 1491 | An alternate definition of "true". (Contributed by Anthony Hart, 13-Oct-2010.) (Revised by BJ, 12-Jul-2019.) (New usage is discouraged.) |
Theorem | trut 1492 | A proposition is equivalent to it being implied by . Closed form of trud 1493. Dual of dfnot 1502. It is to tbtru 1494 what a1bi 352 is to tbt 359. (Contributed by BJ, 26-Oct-2019.) |
Theorem | trud 1493 | Eliminate as an antecedent. A proposition implied by is true. (Contributed by Mario Carneiro, 13-Mar-2014.) |
Theorem | tbtru 1494 | A proposition is equivalent to itself being equivalent to . (Contributed by Anthony Hart, 14-Aug-2011.) |
Theorem | nbfal 1495 | The negation of a proposition is equivalent to itself being equivalent to . (Contributed by Anthony Hart, 14-Aug-2011.) |
Theorem | bitru 1496 | A theorem is equivalent to truth. (Contributed by Mario Carneiro, 9-May-2015.) |
Theorem | bifal 1497 | A contradiction is equivalent to falsehood. (Contributed by Mario Carneiro, 9-May-2015.) |
Theorem | falim 1498 | 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 1499 | The truth value implies anything. (Contributed by Mario Carneiro, 9-Feb-2017.) |
Theorem | a1tru 1500 | Anything implies . (Contributed by FL, 20-Mar-2011.) (Proof shortened by Anthony Hart, 1-Aug-2011.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |