P. 16 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 1501-1600   *Has distinct variable group(s)

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.)
|- ( ( T. /\ ph ) <-> ph )
Theorem	dfnot 1502	Given falsum F., we can define the negation of a wff ph as the statement that F. follows from assuming ph. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 21-Jul-2019.)
|- ( -. ph <-> ( ph -> F. ) )
Theorem	inegd 1503	Negation introduction rule from natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ( ( ph /\ ps ) -> F. )   =>    |- ( ph -> -. ps )
Theorem	efald 1504	Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ( ( ph /\ -. ps ) -> F. )   =>    |- ( ph -> ps )
Theorem	pm2.21fal 1505	If a wff and its negation are provable, then falsum is provable. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ( ph -> ps )   &    |- ( ph -> -. ps )   =>    |- ( ph -> F. )
1.2.14  Truth tables 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 (T.) and false (F.). 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.)
|- ( ( T. /\ T. ) <-> T. )
Theorem	truanfal 1507	A /\ identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( T. /\ F. ) <-> F. )
Theorem	falantru 1508	A /\ identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( F. /\ T. ) <-> F. )
Theorem	falanfal 1509	A /\ identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( F. /\ F. ) <-> F. )
Theorem	truortru 1510	A \/ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( T. \/ T. ) <-> T. )
Theorem	truorfal 1511	A \/ identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( T. \/ F. ) <-> T. )
Theorem	falortru 1512	A \/ identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( F. \/ T. ) <-> T. )
Theorem	falorfal 1513	A \/ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( F. \/ F. ) <-> F. )
Theorem	truimtru 1514	A -> identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( T. -> T. ) <-> T. )
Theorem	truimfal 1515	A -> identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( T. -> F. ) <-> F. )
Theorem	falimtru 1516	A -> identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( F. -> T. ) <-> T. )
Theorem	falimfal 1517	A -> identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( ( F. -> F. ) <-> T. )
Theorem	nottru 1518	A -. identity. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( -. T. <-> F. )
Theorem	notfal 1519	A -. identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( -. F. <-> T. )
Theorem	trubitru 1520	A <-> identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( T. <-> T. ) <-> T. )
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.)
|- ( ( F. <-> T. ) <-> F. )
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.)
|- ( ( T. <-> F. ) <-> F. )
Theorem	falbifal 1523	A <-> identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( F. <-> F. ) <-> T. )
Theorem	trunantru 1524	A -/\ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( T. -/\ T. ) <-> F. )
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.)
|- ( ( T. -/\ F. ) <-> T. )
Theorem	falnantru 1526	A -/\ identity. (Contributed by Anthony Hart, 23-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( F. -/\ T. ) <-> T. )
Theorem	falnanfal 1527	A -/\ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ( F. -/\ F. ) <-> T. )
Theorem	truxortru 1528	A \/_ identity. (Contributed by David A. Wheeler, 8-May-2015.)
|- ( ( T. \/_ T. ) <-> F. )
Theorem	truxorfal 1529	A \/_ identity. (Contributed by David A. Wheeler, 8-May-2015.)
|- ( ( T. \/_ F. ) <-> T. )
Theorem	falxortru 1530	A \/_ identity. (Contributed by David A. Wheeler, 9-May-2015.) (Proof shortened by Wolf Lammen, 10-Jul-2020.)
|- ( ( F. \/_ T. ) <-> T. )
Theorem	falxorfal 1531	A \/_ identity. (Contributed by David A. Wheeler, 9-May-2015.)
|- ( ( F. \/_ F. ) <-> F. )
1.2.15  Half adder and full adder in propositional calculus 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 F. and 1 by T.. Even though hadd and cadd are invariant under permutation of their arguments, assume for the sake of concreteness that ph (resp. ps) 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 ch is the i^th carry (with the convention that the 0^th carry is 0). Then, hadd ( ph , ps , ch ) gives the i^th bit of the sum, and cadd ( ph , ps , ch ) 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.
1.2.15.1  Full adder: sum
Syntax	whad 1532	Syntax for the "sum" output of the full adder. (Contributed by Mario Carneiro, 4-Sep-2016.)
wff hadd ( ph , ps , ch )
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 ( ph , ps , ch ) <-> ( ( ph \/_ ps ) \/_ ch ) )
Theorem	hadbi123d 1534	Equality theorem for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ph -> ( th <-> ta ) )   &    |- ( ph -> ( et <-> ze ) )   =>    |- ( ph -> (hadd ( ps , th , et ) <-> hadd ( ch , ta , ze ) ) )
Theorem	hadbi123i 1535	Equality theorem for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   &    |- ( ta <-> et )   =>    |- (hadd ( ph , ch , ta ) <-> hadd ( ps , th , et ) )
Theorem	hadass 1536	Associative law for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (hadd ( ph , ps , ch ) <-> ( ph \/_ ( ps \/_ ch ) ) )
Theorem	hadbi 1537	The adder sum is the same as the triple biconditional. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (hadd ( ph , ps , ch ) <-> ( ( ph <-> ps ) <-> ch ) )
Theorem	hadcoma 1538	Commutative law for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (hadd ( ph , ps , ch ) <-> hadd ( ps , ph , ch ) )
Theorem	hadcomb 1539	Commutative law for the adders sum. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (hadd ( ph , ps , ch ) <-> hadd ( ph , ch , ps ) )
Theorem	hadrot 1540	Rotation law for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (hadd ( ph , ps , ch ) <-> hadd ( ps , ch , ph ) )
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 ( ph , ps , ch ) <-> hadd ( -. ph , -. ps , -. ch ) )
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.)
|- ( ph -> (hadd ( ph , ps , ch ) <-> ( ps <-> ch ) ) )
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.)
|- ( -. ph -> (hadd ( ph , ps , ch ) <-> ( ps \/_ ch ) ) )
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 ( ph , ps , ch ) <-> if- ( ph , ( ps <-> ch ) , ( ps \/_ ch ) ) )
1.2.15.2  Full adder: carry
Syntax	wcad 1545	Syntax for the "carry" output of the full adder. (Contributed by Mario Carneiro, 4-Sep-2016.)
wff cadd ( ph , ps , ch )
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 ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( ch /\ ( ph \/_ ps ) ) ) )
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 ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( ph /\ ch ) \/ ( ps /\ ch ) ) )
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 ( ph , ps , ch ) <-> ( ( ph \/ ps ) /\ ( ph \/ ch ) /\ ( ps \/ ch ) ) )
Theorem	cadbi123d 1549	Equality theorem for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ph -> ( th <-> ta ) )   &    |- ( ph -> ( et <-> ze ) )   =>    |- ( ph -> (cadd ( ps , th , et ) <-> cadd ( ch , ta , ze ) ) )
Theorem	cadbi123i 1550	Equality theorem for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   &    |- ( ta <-> et )   =>    |- (cadd ( ph , ch , ta ) <-> cadd ( ps , th , et ) )
Theorem	cadcoma 1551	Commutative law for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (cadd ( ph , ps , ch ) <-> cadd ( ps , ph , ch ) )
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 ( ph , ps , ch ) <-> cadd ( ph , ch , ps ) )
Theorem	cadrot 1553	Rotation law for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- (cadd ( ph , ps , ch ) <-> cadd ( ps , ch , ph ) )
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 ( ph , ps , ch ) <-> cadd ( -. ph , -. ps , -. ch ) )
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.)
|- ( ch -> (cadd ( ph , ps , ch ) <-> ( ph \/ ps ) ) )
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.)
|- ( -. ch -> (cadd ( ph , ps , ch ) <-> ( ph /\ ps ) ) )
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 ( ph , ps , ch ) <-> if- ( ch , ( ph \/ ps ) , ( ph /\ ps ) ) )
Theorem	cad11 1558	If (at least) two inputs are true, then the adder carry is true. (Contributed by Mario Carneiro, 4-Sep-2016.)
|- ( ( ph /\ ps ) -> cadd ( ph , ps , ch ) )
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 ( T. , T. , ph )
1.3  Other axiomatizations related to classical propositional calculus
1.3.1  Minimal implicational calculus 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.)
|- ( ph -> ( ( ps -> ch ) -> ( ( ( th -> ps ) -> ( ch -> ta ) ) -> ( ps -> ta ) ) ) )
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.)
|- ( ( ( ph -> ps ) -> ch ) -> ( ps -> ch ) )
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.)
|- ( ph -> ( ps -> ph ) )
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.)
|- ( ( ph -> ps ) -> ( ( ph -> ( ps -> ch ) ) -> ( ph -> ch ) ) )
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.)
|- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) )
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.)
|- ( ( ph -> ( ph -> ps ) ) -> ( ph -> ps ) )
1.3.2  Derive the Lukasiewicz axioms from Meredith's sole axiom
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.)
|- ( ( ( ( ( ph -> ps ) -> ( -. ch -> -. th ) ) -> ch ) -> ta ) -> ( ( ta -> ph ) -> ( th -> ph ) ) )
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.)
|- ( ( ( ch -> ( -. ph -> ps ) ) -> ta ) -> ( ph -> ta ) )
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.)
|- ( ( ( ph -> ph ) -> ch ) -> ( th -> ch ) )
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.)
|- ( ( ( ps -> ch ) -> ph ) -> ( ch -> ph ) )
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.)
|- ( ta -> ( ( ta -> ph ) -> ( th -> ph ) ) )
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.)
|- ( ( ph -> ps ) -> ( -. -. ph -> ps ) )
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.)
|- ( ch -> ( ( ( ps -> ch ) -> ph ) -> ( th -> ph ) ) )
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.)
|- ( ph -> ( ( ( ps -> ch ) -> th ) -> ( ( ( ch -> ta ) -> ( -. th -> -. ps ) ) -> th ) ) )
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.)
|- ( ( ( ps -> ch ) -> th ) -> ( ( ( ch -> ta ) -> ( -. th -> -. ps ) ) -> th ) )
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.)
|- ( ( ( ph -> ps ) -> ( ch -> ( th -> ( ps -> ta ) ) ) ) -> ( et -> ( ch -> ( th -> ( ps -> ta ) ) ) ) )
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.)
|- ( ( ph -> ( ph -> ps ) ) -> ( th -> ( ph -> ps ) ) )
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.)
|- ( ( ph -> ( ph -> ps ) ) -> ( ph -> ps ) )
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.)
|- ( ( ( th -> ( -. -. ch -> ch ) ) -> ph ) -> ph )
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.)
|- ( ( ph -> ps ) -> ( ( ( th -> ( -. -. ch -> ch ) ) -> -. -. ph ) -> ps ) )
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.)
|- ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) )
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.)
|- ( ( -. ph -> ph ) -> ph )
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.)
|- ( ph -> ( -. ph -> ps ) )
1.3.3  Derive the standard axioms from the Lukasiewicz axioms
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.)
|- ( ph -> ps )   &    |- ( ps -> ch )   =>    |- ( ph -> ch )
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.)
|- ( ( ph -> -. ps ) -> ( ( ( ph -> ch ) -> th ) -> ( ps -> th ) ) )
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.)
|- ( ph -> ( ( ( -. ph -> ps ) -> ch ) -> ( th -> ch ) ) )
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.)
|- ( ( ( ( -. ph -> ph ) -> ph ) -> ps ) -> ps )
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.)
|- ( ph -> ( ps -> ph ) )
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.)
|- ( ( ph -> ( ph -> ps ) ) -> ( ph -> ps ) )
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.)
|- ( ( ph -> ( ps -> ch ) ) -> ( ps -> ( ph -> ch ) ) )
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.)
|- ( ( ph -> ps ) -> ( ( ch -> ph ) -> ( ch -> ps ) ) )
Theorem	ax1 1591	Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> ( ps -> ph ) )
Theorem	ax2 1592	Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) )
Theorem	ax3 1593	Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( -. ph -> -. ps ) -> ( ps -> ph ) )
1.3.4  Derive Nicod's axiom from the standard axioms Prove Nicod's axiom and implication and negation definitions.
Theorem	nic-dfim 1594	Define implication in terms of 'nand'. Analogous to ( ( ph -/\ ( ps -/\ ps ) ) <-> ( ph -> ps ) ). 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.)
|- ( ( ( ph -/\ ( ps -/\ ps ) ) -/\ ( ph -> ps ) ) -/\ ( ( ( ph -/\ ( ps -/\ ps ) ) -/\ ( ph -/\ ( ps -/\ ps ) ) ) -/\ ( ( ph -> ps ) -/\ ( ph -> ps ) ) ) )
Theorem	nic-dfneg 1595	Define negation in terms of 'nand'. Analogous to ( ( ph -/\ ph ) <-> -. ph ). 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.)
|- ( ( ( ph -/\ ph ) -/\ -. ph ) -/\ ( ( ( ph -/\ ph ) -/\ ( ph -/\ ph ) ) -/\ ( -. ph -/\ -. ph ) ) )
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 ch, 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.)
|- ph   &    |- ( ph -/\ ( ch -/\ ps ) )   =>    |- ps
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.)
|- ph   &    |- ( ph -/\ ( ch -/\ ps ) )   =>    |- ps
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.)
|- ( ( ph -/\ ( ch -/\ ps ) ) -/\ ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )
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.)
|- ( ( ph -/\ ( ch -/\ ps ) ) -/\ ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )
1.3.5  Derive the Lukasiewicz axioms from Nicod's axiom
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.)
|- ( ph -/\ ( ch -/\ ps ) )   =>    |- ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) )