P. 18 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 1701-1800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	trunanfal 1701	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 1702	A ⊼ identity. (Contributed by Anthony Hart, 23-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ ((⊥ ⊼ ⊤) ↔ ⊤)
Theorem	falnanfal 1703	A ⊼ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ ((⊥ ⊼ ⊥) ↔ ⊤)
1.2.15.7  Exclusive disjunction
Theorem	truxortru 1704	A ⊻ identity. (Contributed by David A. Wheeler, 8-May-2015.)
⊢ ((⊤ ⊻ ⊤) ↔ ⊥)
Theorem	truxorfal 1705	A ⊻ identity. (Contributed by David A. Wheeler, 8-May-2015.)
⊢ ((⊤ ⊻ ⊥) ↔ ⊤)
Theorem	falxortru 1706	A ⊻ identity. (Contributed by David A. Wheeler, 9-May-2015.) (Proof shortened by Wolf Lammen, 10-Jul-2020.)
⊢ ((⊥ ⊻ ⊤) ↔ ⊤)
Theorem	falxorfal 1707	A ⊻ identity. (Contributed by David A. Wheeler, 9-May-2015.)
⊢ ((⊥ ⊻ ⊥) ↔ ⊥)
1.2.16  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 1640) and the logical conjunction (df-an 387). The full adder takes into account an "input carry", so it has three inputs and again two outputs, corresponding to the "sum" (df-had 1709) and "updated carry" (df-cad 1722). 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.
1.2.16.1  Full adder: sum
Syntax	whad 1708	Syntax for the "sum" output of the full adder. (Contributed by Mario Carneiro, 4-Sep-2016.)
wff hadd(𝜑, 𝜓, 𝜒)
Definition	df-had 1709	Definition of the "sum" output of the full adder (triple exclusive disjunction, or XOR3). (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ⊻ 𝜓) ⊻ 𝜒))
Theorem	hadbi123d 1710	Equality theorem for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    &   ⊢ (𝜑 → (𝜂 ↔ 𝜁))    ⇒   ⊢ (𝜑 → (hadd(𝜓, 𝜃, 𝜂) ↔ hadd(𝜒, 𝜏, 𝜁)))
Theorem	hadbi123i 1711	Equality theorem for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    &   ⊢ (𝜏 ↔ 𝜂)    ⇒   ⊢ (hadd(𝜑, 𝜒, 𝜏) ↔ hadd(𝜓, 𝜃, 𝜂))
Theorem	hadass 1712	Associative law for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ⊻ (𝜓 ⊻ 𝜒)))
Theorem	hadbi 1713	The adder sum is the same as the triple biconditional. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ↔ 𝜓) ↔ 𝜒))
Theorem	hadcoma 1714	Commutative law for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ hadd(𝜓, 𝜑, 𝜒))
Theorem	hadcomb 1715	Commutative law for the adders sum. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ hadd(𝜑, 𝜒, 𝜓))
Theorem	hadrot 1716	Rotation law for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ hadd(𝜓, 𝜒, 𝜑))
Theorem	hadnot 1717	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 1718	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 1719	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 1720	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-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒)))
1.2.16.2  Full adder: carry
Syntax	wcad 1721	Syntax for the "carry" output of the full adder. (Contributed by Mario Carneiro, 4-Sep-2016.)
wff cadd(𝜑, 𝜓, 𝜒)
Definition	df-cad 1722	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 1723 and cadan 1724 for alternate definitions. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓))))
Theorem	cador 1723	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 1724	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 1725	Equality theorem for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    &   ⊢ (𝜑 → (𝜂 ↔ 𝜁))    ⇒   ⊢ (𝜑 → (cadd(𝜓, 𝜃, 𝜂) ↔ cadd(𝜒, 𝜏, 𝜁)))
Theorem	cadbi123i 1726	Equality theorem for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    &   ⊢ (𝜏 ↔ 𝜂)    ⇒   ⊢ (cadd(𝜑, 𝜒, 𝜏) ↔ cadd(𝜓, 𝜃, 𝜂))
Theorem	cadcoma 1727	Commutative law for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ cadd(𝜓, 𝜑, 𝜒))
Theorem	cadcomb 1728	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 1729	Rotation law for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ cadd(𝜓, 𝜒, 𝜑))
Theorem	cadnot 1730	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 1731	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 1732	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 1733	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 1734	If (at least) two inputs are true, then the adder carry is true. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ ((𝜑 ∧ 𝜓) → cadd(𝜑, 𝜓, 𝜒))
Theorem	cadtru 1735	The adder carry is true as soon as its first two inputs are the truth constant. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ cadd(⊤, ⊤, 𝜑)
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 1736. This section proves minimp 1736 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 1736	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. Among single axioms of this length, it is the one with simplest antecedents (i.e., in the corresponding ordering of binary trees which first compares left subtrees, it is the first one). (Contributed by BJ, 4-Apr-2021.)
⊢ (𝜑 → ((𝜓 → 𝜒) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → 𝜏))))
Theorem	minimp-syllsimp 1737	Derivation of Syll-Simp (jarr 106) from ax-mp 5 and minimp 1736. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒))
Theorem	minimp-ax1 1738	Derivation of ax-1 6 from ax-mp 5 and minimp 1736. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜑))
Theorem	minimp-ax2c 1739	Derivation of a commuted form of ax-2 7 from ax-mp 5 and minimp 1736. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))
Theorem	minimp-ax2 1740	Derivation of ax-2 7 from ax-mp 5 and minimp 1736. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
Theorem	minimp-pm2.43 1741	Derivation of pm2.43 56 (also called "hilbert" or W) from ax-mp 5 and minimp 1736. 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.)
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓))
1.3.2  Derive the Lukasiewicz axioms from Meredith's sole axiom
Theorem	meredith 1742	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 1756, luk-2 1757, and luk-3 1758. Using these we finally rederive our axioms as ax1 1767, ax2 1768, and ax3 1769, 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 1743	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 1744	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 1745	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 1746	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 1747	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 1748	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 1749	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 1750	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 1751	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 1752	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 1753	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 1754	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 1755	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 1756	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 1757	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 1758	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.)
⊢ (𝜑 → (¬ 𝜑 → 𝜓))
1.3.3  Derive the standard axioms from the Lukasiewicz axioms
Theorem	luklem1 1759	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 23-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	luklem2 1760	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → ¬ 𝜓) → (((𝜑 → 𝜒) → 𝜃) → (𝜓 → 𝜃)))
Theorem	luklem3 1761	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (((¬ 𝜑 → 𝜓) → 𝜒) → (𝜃 → 𝜒)))
Theorem	luklem4 1762	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((¬ 𝜑 → 𝜑) → 𝜑) → 𝜓) → 𝜓)
Theorem	luklem5 1763	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜑))
Theorem	luklem6 1764	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓))
Theorem	luklem7 1765	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))
Theorem	luklem8 1766	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜑) → (𝜒 → 𝜓)))
Theorem	ax1 1767	Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜑))
Theorem	ax2 1768	Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
Theorem	ax3 1769	Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))
1.3.4  Derive Nicod's axiom from the standard axioms Prove Nicod's axiom and implication and negation definitions.
Theorem	nic-dfim 1770	This theorem "defines" implication in terms of 'nand'. Analogous to nanim 1623. 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 1771	This theorem "defines" negation in terms of 'nand'. Analogous to nannot 1624. 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 1772	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 1774. 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 1773	A direct proof of nic-mp 1772. (Contributed by NM, 30-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓))    ⇒   ⊢ 𝜓
Theorem	nic-ax 1774	Nicod's axiom derived from the standard ones. See Introduction to Mathematical Philosophy by B. Russell, p. 152. Like meredith 1742, the usual axioms can be derived from this and vice versa. Unlike meredith 1742, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g. { nic-ax 1774, nic-mp 1772 } is equivalent to { luk-1 1756, luk-2 1757, luk-3 1758, 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 1775	A direct proof of nic-ax 1774. (Contributed by NM, 11-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))
1.3.5  Derive the Lukasiewicz axioms from Nicod's axiom
Theorem	nic-imp 1776	Inference for nic-mp 1772 using nic-ax 1774 as major premise. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓))    ⇒   ⊢ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))
Theorem	nic-idlem1 1777	Lemma for nic-id 1779. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜃 ⊼ (𝜏 ⊼ (𝜏 ⊼ 𝜏))) ⊼ (((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ 𝜃) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ 𝜃)))
Theorem	nic-idlem2 1778	Lemma for nic-id 1779. Inference used by nic-id 1779. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜂 ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ 𝜃))    ⇒   ⊢ ((𝜃 ⊼ (𝜏 ⊼ (𝜏 ⊼ 𝜏))) ⊼ 𝜂)
Theorem	nic-id 1779	Theorem id 22 expressed with ⊼. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜏 ⊼ (𝜏 ⊼ 𝜏))
Theorem	nic-swap 1780	The connector ⊼ is symmetric. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜃 ⊼ 𝜑) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))
Theorem	nic-isw1 1781	Inference version of nic-swap 1780. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜃 ⊼ 𝜑)    ⇒   ⊢ (𝜑 ⊼ 𝜃)
Theorem	nic-isw2 1782	Inference for swapping nested terms. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜓 ⊼ (𝜃 ⊼ 𝜑))    ⇒   ⊢ (𝜓 ⊼ (𝜑 ⊼ 𝜃))
Theorem	nic-iimp1 1783	Inference version of nic-imp 1776 using right-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓))    &   ⊢ (𝜃 ⊼ 𝜒)    ⇒   ⊢ (𝜃 ⊼ 𝜑)
Theorem	nic-iimp2 1784	Inference version of nic-imp 1776 using left-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ⊼ 𝜓) ⊼ (𝜒 ⊼ 𝜒))    &   ⊢ (𝜃 ⊼ 𝜑)    ⇒   ⊢ (𝜃 ⊼ (𝜒 ⊼ 𝜒))
Theorem	nic-idel 1785	Inference to remove the trailing term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓))    ⇒   ⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜒))
Theorem	nic-ich 1786	Chained inference. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ⊼ (𝜓 ⊼ 𝜓))    &   ⊢ (𝜓 ⊼ (𝜒 ⊼ 𝜒))    ⇒   ⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜒))
Theorem	nic-idbl 1787	Double the terms. Since doubling is the same as negation, this can be viewed as a contraposition inference. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ⊼ (𝜓 ⊼ 𝜓))    ⇒   ⊢ ((𝜓 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜑) ⊼ (𝜑 ⊼ 𝜑)))
Theorem	nic-bijust 1788	Biconditional justification from Nicod's axiom. For nic-* definitions, the biconditional connective is not used. Instead, definitions are made based on this form. nic-bi1 1789 and nic-bi2 1790 are used to convert the definitions into usable theorems about one side of the implication. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜏 ⊼ 𝜏) ⊼ ((𝜏 ⊼ 𝜏) ⊼ (𝜏 ⊼ 𝜏)))
Theorem	nic-bi1 1789	Inference to extract one side of an implication from a definition. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜑) ⊼ (𝜓 ⊼ 𝜓)))    ⇒   ⊢ (𝜑 ⊼ (𝜓 ⊼ 𝜓))
Theorem	nic-bi2 1790	Inference to extract the other side of an implication from a 'biconditional' definition. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜑) ⊼ (𝜓 ⊼ 𝜓)))    ⇒   ⊢ (𝜓 ⊼ (𝜑 ⊼ 𝜑))
Theorem	nic-stdmp 1791	Derive the standard modus ponens from nic-mp 1772. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ 𝜓
Theorem	nic-luk1 1792	Proof of luk-1 1756 from nic-ax 1774 and nic-mp 1772 (and definitions nic-dfim 1770 and nic-dfneg 1771). Note that the standard axioms ax-1 6, ax-2 7, and ax-3 8 are proved from the Lukasiewicz axioms by theorems ax1 1767, ax2 1768, and ax3 1769. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
Theorem	nic-luk2 1793	Proof of luk-2 1757 from nic-ax 1774 and nic-mp 1772. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((¬ 𝜑 → 𝜑) → 𝜑)
Theorem	nic-luk3 1794	Proof of luk-3 1758 from nic-ax 1774 and nic-mp 1772. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (¬ 𝜑 → 𝜓))
1.3.6  Derive Nicod's Axiom from Lukasiewicz's First Sheffer Stroke Axiom
Theorem	lukshef-ax1 1795	This alternative axiom for propositional calculus using the Sheffer Stroke was discovered by Lukasiewicz in his Selected Works. It improves on Nicod's axiom by reducing its number of variables by one. This axiom also uses nic-mp 1772 for its constructions. Here, the axiom is proved as a substitution instance of nic-ax 1774. (Contributed by Anthony Hart, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜃 ⊼ (𝜃 ⊼ 𝜃)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))
Theorem	lukshefth1 1796	Lemma for renicax 1798. (Contributed by NM, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((𝜏 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜏) ⊼ (𝜑 ⊼ 𝜏))) ⊼ (𝜃 ⊼ (𝜃 ⊼ 𝜃))) ⊼ (𝜑 ⊼ (𝜓 ⊼ 𝜒)))
Theorem	lukshefth2 1797	Lemma for renicax 1798. (Contributed by NM, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜏 ⊼ 𝜃) ⊼ ((𝜃 ⊼ 𝜏) ⊼ (𝜃 ⊼ 𝜏)))
Theorem	renicax 1798	A rederivation of nic-ax 1774 from lukshef-ax1 1795, proving that lukshef-ax1 1795 with nic-mp 1772 can be used as a complete axiomatization of propositional calculus. (Contributed by Anthony Hart, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))
1.3.7  Derive the Lukasiewicz Axioms from the Tarski-Bernays-Wajsberg Axioms
Theorem	tbw-bijust 1799	Justification for tbw-negdf 1800. (Contributed by Anthony Hart, 15-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ↔ 𝜓) ↔ (((𝜑 → 𝜓) → ((𝜓 → 𝜑) → ⊥)) → ⊥))
Theorem	tbw-negdf 1800	The definition of negation, in terms of → and ⊥. (Contributed by Anthony Hart, 15-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((¬ 𝜑 → (𝜑 → ⊥)) → (((𝜑 → ⊥) → ¬ 𝜑) → ⊥)) → ⊥)