Home | Metamath
Proof Explorer Theorem List (p. 16 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 | truan 1501 | True can be removed from a conjunction. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Wolf Lammen, 21-Jul-2019.) |
Theorem | dfnot 1502 | 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 1503 | Negation introduction rule from natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.) |
Theorem | efald 1504 | Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.) |
Theorem | pm2.21fal 1505 | 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 386, (disjunction aka logical inclusive 'or') df-or 385, (implies) wi 4, (not) wn 3, (logical equivalence) df-bi 197, (nand aka Sheffer stroke) df-nan 1448, and (exclusive or) df-xor 1465. | ||
Theorem | truantru 1506 | A identity. (Contributed by Anthony Hart, 22-Oct-2010.) |
Theorem | truanfal 1507 | A identity. (Contributed by Anthony Hart, 22-Oct-2010.) |
Theorem | falantru 1508 | A identity. (Contributed by Anthony Hart, 22-Oct-2010.) |
Theorem | falanfal 1509 | A identity. (Contributed by Anthony Hart, 22-Oct-2010.) |
Theorem | truortru 1510 | A identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Theorem | truorfal 1511 | A identity. (Contributed by Anthony Hart, 22-Oct-2010.) |
Theorem | falortru 1512 | A identity. (Contributed by Anthony Hart, 22-Oct-2010.) |
Theorem | falorfal 1513 | A identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Theorem | truimtru 1514 | A identity. (Contributed by Anthony Hart, 22-Oct-2010.) |
Theorem | truimfal 1515 | A identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Theorem | falimtru 1516 | A identity. (Contributed by Anthony Hart, 22-Oct-2010.) |
Theorem | falimfal 1517 | A identity. (Contributed by Anthony Hart, 22-Oct-2010.) |
Theorem | nottru 1518 | A identity. (Contributed by Anthony Hart, 22-Oct-2010.) |
Theorem | notfal 1519 | A identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Theorem | trubitru 1520 | A identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Theorem | falbitru 1521 | A identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 10-Jul-2020.) |
Theorem | trubifal 1522 | A identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 10-Jul-2020.) |
Theorem | falbifal 1523 | A identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Theorem | trunantru 1524 | A identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Theorem | trunanfal 1525 | A identity. (Contributed by Anthony Hart, 23-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 10-Jul-2020.) |
Theorem | falnantru 1526 | A identity. (Contributed by Anthony Hart, 23-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Theorem | falnanfal 1527 | A identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Theorem | truxortru 1528 | A identity. (Contributed by David A. Wheeler, 8-May-2015.) |
Theorem | truxorfal 1529 | A identity. (Contributed by David A. Wheeler, 8-May-2015.) |
Theorem | falxortru 1530 | A identity. (Contributed by David A. Wheeler, 9-May-2015.) (Proof shortened by Wolf Lammen, 10-Jul-2020.) |
Theorem | falxorfal 1531 | A identity. (Contributed by David A. Wheeler, 9-May-2015.) |
Propositional calculus deals with truth values, which can be interpreted as bits. Using this, we can define the half adder and the full adder in pure propositional calculus, and show their basic properties. The half adder adds two 1-bit numbers. Its two outputs are the "sum" S and the "carry" C. The real sum is then given by 2C+S. The sum and carry correspond respectively to the logical exclusive disjunction (df-xor 1465) and the logical conjunction (df-an 386). The full adder takes into account an "input carry", so it has three inputs and again two outputs, corresponding to the "sum" (df-had 1533) and "updated carry" (df-cad 1546). Here is a short description. We code the bit 0 by and 1 by . Even though hadd and cadd are invariant under permutation of their arguments, assume for the sake of concreteness that (resp. ) is the i^th bit of the first (resp. second) number to add (with the convention that the i^th bit is the multiple of 2^i in the base-2 representation), and that is the i^th carry (with the convention that the 0^th carry is 0). Then, hadd gives the i^th bit of the sum, and cadd gives the (i+1)^th carry. Then, addition is performed by iteration from i = 0 to i = 1 + (max of the number of digits of the two summands) by "updating" the carry. | ||
Syntax | whad 1532 | Syntax for the "sum" output of the full adder. (Contributed by Mario Carneiro, 4-Sep-2016.) |
hadd | ||
Definition | df-had 1533 | Definition of the "sum" output of the full adder (triple exclusive disjunction, or XOR3). (Contributed by Mario Carneiro, 4-Sep-2016.) |
hadd | ||
Theorem | hadbi123d 1534 | Equality theorem for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016.) |
hadd hadd | ||
Theorem | hadbi123i 1535 | Equality theorem for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016.) |
hadd hadd | ||
Theorem | hadass 1536 | Associative law for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016.) |
hadd | ||
Theorem | hadbi 1537 | The adder sum is the same as the triple biconditional. (Contributed by Mario Carneiro, 4-Sep-2016.) |
hadd | ||
Theorem | hadcoma 1538 | Commutative law for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016.) |
hadd hadd | ||
Theorem | hadcomb 1539 | Commutative law for the adders sum. (Contributed by Mario Carneiro, 4-Sep-2016.) |
hadd hadd | ||
Theorem | hadrot 1540 | Rotation law for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016.) |
hadd hadd | ||
Theorem | hadnot 1541 | The adder sum distributes over negation. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 11-Jul-2020.) |
hadd hadd | ||
Theorem | had1 1542 | If the first input is true, then the adder sum is equivalent to the biconditionality of the other two inputs. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 11-Jul-2020.) |
hadd | ||
Theorem | had0 1543 | If the first input is false, then the adder sum is equivalent to the exclusive disjunction of the other two inputs. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 12-Jul-2020.) |
hadd | ||
Theorem | hadifp 1544 | The value of the adder sum is, if the first input is true, the biconditionality, and if the first input is false, the exclusive disjunction, of the other two inputs. (Contributed by BJ, 11-Aug-2020.) |
hadd if- | ||
Syntax | wcad 1545 | Syntax for the "carry" output of the full adder. (Contributed by Mario Carneiro, 4-Sep-2016.) |
cadd | ||
Definition | df-cad 1546 | Definition of the "carry" output of the full adder. It is true when at least two arguments are true, so it is equal to the "majority" function on three variables. See cador 1547 and cadan 1548 for alternate definitions. (Contributed by Mario Carneiro, 4-Sep-2016.) |
cadd | ||
Theorem | cador 1547 | The adder carry in disjunctive normal form. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 11-Jul-2020.) |
cadd | ||
Theorem | cadan 1548 | The adder carry in conjunctive normal form. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 25-Sep-2018.) |
cadd | ||
Theorem | cadbi123d 1549 | Equality theorem for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.) |
cadd cadd | ||
Theorem | cadbi123i 1550 | Equality theorem for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.) |
cadd cadd | ||
Theorem | cadcoma 1551 | Commutative law for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.) |
cadd cadd | ||
Theorem | cadcomb 1552 | Commutative law for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 11-Jul-2020.) |
cadd cadd | ||
Theorem | cadrot 1553 | Rotation law for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.) |
cadd cadd | ||
Theorem | cadnot 1554 | The adder carry distributes over negation. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 11-Jul-2020.) |
cadd cadd | ||
Theorem | cad1 1555 | If one input is true, then the adder carry is true exactly when at least one of the other two inputs is true. (Contributed by Mario Carneiro, 8-Sep-2016.) (Proof shortened by Wolf Lammen, 19-Jun-2020.) |
cadd | ||
Theorem | cad0 1556 | If one input is false, then the adder carry is true exactly when both of the other two inputs are true. (Contributed by Mario Carneiro, 8-Sep-2016.) |
cadd | ||
Theorem | cadifp 1557 | The value of the carry is, if the input carry is true, the disjunction, and if the input carry is false, the conjunction, of the other two inputs. (Contributed by BJ, 8-Oct-2019.) |
cadd if- | ||
Theorem | cad11 1558 | If (at least) two inputs are true, then the adder carry is true. (Contributed by Mario Carneiro, 4-Sep-2016.) |
cadd | ||
Theorem | cadtru 1559 | The adder carry is true as soon as its first two inputs are the truth constant. (Contributed by Mario Carneiro, 4-Sep-2016.) |
cadd | ||
Minimal implicational calculus, or intuitionistic implicational calculus, or positive implicational calculus, is the implicational fragment of minimal calculus (which is also the implicational fragment of intuitionistic calculus and of positive calculus). It is sometimes called "C-pure intuitionism" since the letter C is sometimes used to denote implication, especially in prefix notation. It can be axiomatized by the inference rule of modus ponens ax-mp 5 together with the axioms { ax-1 6, ax-2 7 } (sometimes written KS), or with { imim1 83, ax-1 6, pm2.43 56 } (written B'KW), or with { imim2 58, pm2.04 90, ax-1 6, pm2.43 56 } (written BCKW), or with the single axiom minimp 1560. This section proves minimp 1560 from { ax-1 6, ax-2 7 }, and then the converse, due to Ivo Thomas. Sources for this section are the webpage https://web.ics.purdue.edu/~dulrich/C-pure-intuitionism-page.htm on Ted Ulrich's website, and the articles C. A. Meredith, A single axiom of positive logic, Journal of computing systems, vol. 1 (1953), 169--170, and C. A. Meredith, A. N. Prior, Notes on the axiomatics of the propositional calculus, Notre Dame Journal of Formal Logic, vol. 4 (1963), 171--187. We may use a compact notation for derivations known as the D-notation where "D" stands for "condensed Detachment". For instance, "D21" means detaching ax-1 6 from ax-2 7, that is, using modus ponens ax-mp 5 with ax-1 6 as minor premise and ax-2 7 as major premise. D-strings are accepted by the grammar Dstr := digit | "D" Dstr Dstr. (Contributed by BJ, 11-Apr-2021.) | ||
Theorem | minimp 1560 | A single axiom for minimal implicational calculus, due to Meredith. Other single axioms of the same length are known, but it is thought to be the minimal length. (Contributed by BJ, 4-Apr-2021.) |
Theorem | minimp-sylsimp 1561 | Derivation of sylsimp (jarr 106) from ax-mp 5 and minimp 1560. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | minimp-ax1 1562 | Derivation of ax-1 6 from ax-mp 5 and minimp 1560. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | minimp-ax2c 1563 | Derivation of a commuted form of ax-2 7 from ax-mp 5 and minimp 1560. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | minimp-ax2 1564 | Derivation of ax-2 7 from ax-mp 5 and minimp 1560. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | minimp-pm2.43 1565 | Derivation of pm2.43 56 (also called "hilbert" or W) from ax-mp 5 and minimp 1560. It uses the classical derivation from ax-1 6 and ax-2 7 written DD22D21 in D-notation (see head comment for an explanation) and shortens the proof using mp2 9 (which only requires ax-mp 5). (Contributed by BJ, 31-May-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | meredith 1566 |
Carew Meredith's sole axiom for propositional calculus. This amazing
formula is thought to be the shortest possible single axiom for
propositional calculus with inference rule ax-mp 5,
where negation and
implication are primitive. Here we prove Meredith's axiom from ax-1 6,
ax-2 7, and ax-3 8. Then from it we derive the Lukasiewicz
axioms
luk-1 1580, luk-2 1581, and luk-3 1582. Using these we finally rederive our
axioms as ax1 1591, ax2 1592, and ax3 1593,
thus proving the equivalence of all
three systems. C. A. Meredith, "Single Axioms for the Systems (C,N),
(C,O) and (A,N) of the Two-Valued Propositional Calculus," The
Journal of
Computing Systems vol. 1 (1953), pp. 155-164. Meredith claimed to be
close to a proof that this axiom is the shortest possible, but the proof
was apparently never completed.
An obscure Irish lecturer, Meredith (1904-1976) became enamored with logic somewhat late in life after attending talks by Lukasiewicz and produced many remarkable results such as this axiom. From his obituary: "He did logic whenever time and opportunity presented themselves, and he did it on whatever materials came to hand: in a pub, his favored pint of porter within reach, he would use the inside of cigarette packs to write proofs for logical colleagues." (Contributed by NM, 14-Dec-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (Proof shortened by Wolf Lammen, 28-May-2013.) |
Theorem | merlem1 1567 | Step 3 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (The step numbers refer to Meredith's original paper.) (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | merlem2 1568 | Step 4 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | merlem3 1569 | Step 7 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | merlem4 1570 | Step 8 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | merlem5 1571 | Step 11 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | merlem6 1572 | Step 12 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | merlem7 1573 | Between steps 14 and 15 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | merlem8 1574 | Step 15 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | merlem9 1575 | Step 18 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | merlem10 1576 | Step 19 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | merlem11 1577 | Step 20 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | merlem12 1578 | Step 28 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | merlem13 1579 | Step 35 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | luk-1 1580 | 1 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | luk-2 1581 | 2 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | luk-3 1582 | 3 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | luklem1 1583 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 23-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | luklem2 1584 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | luklem3 1585 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | luklem4 1586 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | luklem5 1587 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | luklem6 1588 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | luklem7 1589 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | luklem8 1590 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ax1 1591 | Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ax2 1592 | Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | ax3 1593 | Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Prove Nicod's axiom and implication and negation definitions. | ||
Theorem | nic-dfim 1594 | Define implication in terms of 'nand'. Analogous to . In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to a definition ($a statement). (Contributed by NM, 11-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | nic-dfneg 1595 | Define negation in terms of 'nand'. Analogous to . In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to a definition ($a statement). (Contributed by NM, 11-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | nic-mp 1596 | Derive Nicod's rule of modus ponens using 'nand', from the standard one. Although the major and minor premise together also imply , this form is necessary for useful derivations from nic-ax 1598. In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to an axiom ($a statement). (Contributed by Jeff Hoffman, 19-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | nic-mpALT 1597 | A direct proof of nic-mp 1596. (Contributed by NM, 30-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | nic-ax 1598 | Nicod's axiom derived from the standard ones. See Introduction to Mathematical Philosophy by B. Russell, p. 152. Like meredith 1566, the usual axioms can be derived from this and vice versa. Unlike meredith 1566, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g. nic-ax 1598, nic-mp 1596 is equivalent to luk-1 1580, luk-2 1581, luk-3 1582, ax-mp 5 . In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to an axiom ($a statement). (Contributed by Jeff Hoffman, 19-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | nic-axALT 1599 | A direct proof of nic-ax 1598. (Contributed by NM, 11-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | nic-imp 1600 | Inference for nic-mp 1596 using nic-ax 1598 as major premise. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |