P. 17 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 1601-1700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	had0 1601	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 1602	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.17.2  Full adder: carry
Syntax	wcad 1603	Syntax for the "carry" output of the full adder. (Contributed by Mario Carneiro, 4-Sep-2016.)
wff cadd(𝜑, 𝜓, 𝜒)
Definition	df-cad 1604	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 1605 and cadan 1606 for alternate definitions. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓))))
Theorem	cador 1605	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 1606	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 1607	Equality theorem for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    &   ⊢ (𝜑 → (𝜂 ↔ 𝜁))    ⇒   ⊢ (𝜑 → (cadd(𝜓, 𝜃, 𝜂) ↔ cadd(𝜒, 𝜏, 𝜁)))
Theorem	cadbi123i 1608	Equality theorem for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    &   ⊢ (𝜏 ↔ 𝜂)    ⇒   ⊢ (cadd(𝜑, 𝜒, 𝜏) ↔ cadd(𝜓, 𝜃, 𝜂))
Theorem	cadcoma 1609	Commutative law for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ cadd(𝜓, 𝜑, 𝜒))
Theorem	cadcomb 1610	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 1611	Rotation law for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ cadd(𝜓, 𝜒, 𝜑))
Theorem	cadnot 1612	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 1613	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 1614	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 1615	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 1616	If (at least) two inputs are true, then the adder carry is true. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ ((𝜑 ∧ 𝜓) → cadd(𝜑, 𝜓, 𝜒))
Theorem	cadtru 1617	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 1618. This section proves minimp 1618 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 7 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 1618	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 1619	Derivation of Syll-Simp (jarr 106) from ax-mp 5 and minimp 1618. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒))
Theorem	minimp-ax1 1620	Derivation of ax-1 6 from ax-mp 5 and minimp 1618. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜑))
Theorem	minimp-ax2c 1621	Derivation of a commuted form of ax-2 7 from ax-mp 5 and minimp 1618. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒)))
Theorem	minimp-ax2 1622	Derivation of ax-2 7 from ax-mp 5 and minimp 1618. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
Theorem	minimp-pm2.43 1623	Derivation of pm2.43 56 (also called "hilbert" or W) from ax-mp 5 and minimp 1618. 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  Implicational Calculus Implicational calculus is the fragment of propositional logic that uses only material implication, and not negation. It can be axiomatized by inference rule modus ponens ax-mp 5 together with the axioms { ax-1 6, ax-2 7, peirce 204 } or the Tarski-Bernays axioms { ax-1 6, imim1 83, peirce 204 } or with the single axiom { impsingle 1624 }. From either one of these three axiom sets, all tautologies containing only material implication may be proved. In contrast, minimal implicational calculus, which is presented just before this section, cannot prove certain tautologies (peirce 204, for example ). The class of theorems proved by minimal implicational calculus is thus a subset of the class of theorems proved by implicational calculus. The primary source for this section is the paper by Lukasiewicz, The Shortest Axiom of the Implicational Calculus of Propositions, Proceedings of the Royal Irish Academy, Section A, vol. 52 (1948-1950), 25--33. It will be cited as simply "Lukasiewicz" in the remainder of this section. This section proves that the above three distinct axiom sets for implicational calculus all produce the same class of theorems. (Contributed by Larry Lesyna and Jeffrey P. Machado, 1-Aug-2023.)
Theorem	impsingle 1624	The shortest single axiom for implicational calculus, due to Lukasiewicz. It is now known to be the unique shortest axiom. The axiom is proved here starting from { ax-1 6, ax-2 7 and peirce 204 }. (Contributed by Larry Lesyna and Jeffrey P. Machado, 18-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜒) → ((𝜒 → 𝜑) → (𝜃 → 𝜑)))
Theorem	impsingle-step4 1625	Derivation of impsingle-step4 from ax-mp 5 and impsingle 1624. It is used as a lemma in proofs of imim1 83 and peirce 204 from impsingle 1624. It is Step 4 in Lukasiewicz, where it appears as 'CCCpqpCsp' using parenthesis-free prefix notation. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜑) → (𝜒 → 𝜑))
Theorem	impsingle-step8 1626	Derivation of impsingle-step8 from ax-mp 5 and impsingle 1624. It is used as a lemma in proofs of ax-1 6 imim1 83 and peirce 204 from impsingle 1624. It is Step 8 in Lukasiewicz, where it appears as 'CCCsqpCqp' using parenthesis-free prefix notation. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒))
Theorem	impsingle-ax1 1627	Derivation of impsingle-ax1 (ax-1 6) from ax-mp 5 and impsingle 1624. Lukasiewicz was used to construct this proof. Every formula corresponding to a detachment step was converted to its corresponding Metamath formula. mmj2 was used to unify each formula using ax-mp 5, which in turn produced this proof. With extremely high confidence, this result shows that the Lukasiewicz proof of ax-1 6 (step 27) is correct and that Metamath correctly verifies the proof. The same comments apply to the proofs that follow this one. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜑))
Theorem	impsingle-step15 1628	Derivation of impsingle-step15 from ax-mp 5 and impsingle 1624. It is used as a lemma in proofs of imim1 83 and peirce 204 from impsingle 1624. It is Step 15 in Lukasiewicz, where it appears as 'CCCrqCspCCrpCsp' using parenthesis-free prefix notation. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → (𝜒 → 𝜃)) → ((𝜑 → 𝜃) → (𝜒 → 𝜃)))
Theorem	impsingle-step18 1629	Derivation of impsingle-step18 from ax-mp 5 and impsingle 1624. It is used as a lemma in proofs of imim1 83 and peirce 204 from impsingle 1624. It is Step 18 in Lukasiewicz, where it appears as 'CCCCrpCspCCCpqrtCuCCCpqrt' using parenthesis-free prefix notation. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((𝜑 → 𝜓) → (𝜒 → 𝜓)) → (((𝜓 → 𝜃) → 𝜑) → 𝜏)) → (𝜂 → (((𝜓 → 𝜃) → 𝜑) → 𝜏)))
Theorem	impsingle-step19 1630	Derivation of impsingle-step19 from ax-mp 5 and impsingle 1624. It is used as a lemma in proofs of imim1 83 and peirce 204 from impsingle 1624. It is Step 19 in Lukasiewicz, where it appears as 'CCCCspqCrpCCCpqrCsp' using parenthesis-free prefix notation. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((𝜑 → 𝜓) → 𝜒) → (𝜃 → 𝜓)) → (((𝜓 → 𝜒) → 𝜃) → (𝜑 → 𝜓)))
Theorem	impsingle-step20 1631	Derivation of impsingle-step20 from ax-mp 5 and impsingle 1624. It is used as a lemma in proofs of imim1 83 and peirce 204 from impsingle 1624. It is Step 20 in Lukasiewicz, where it appears as 'CCCCrppCspCCCpqrCsp' using parenthesis-free prefix notation. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((𝜑 → 𝜓) → 𝜓) → (𝜒 → 𝜓)) → (((𝜓 → 𝜃) → 𝜑) → (𝜒 → 𝜓)))
Theorem	impsingle-step21 1632	Derivation of impsingle-step21 from ax-mp 5 and impsingle 1624. It is used as a lemma in the proof of imim1 83 from impsingle 1624. It is Step 21 in Lukasiewicz, where it appears as 'CCCCprqqCCqrCpr' using parenthesis-free prefix notation. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((𝜑 → 𝜓) → 𝜒) → 𝜒) → ((𝜒 → 𝜓) → (𝜑 → 𝜓)))
Theorem	impsingle-step22 1633	Derivation of impsingle-step22 from ax-mp 5 and impsingle 1624. It is used as a lemma in proofs of imim1 83 and peirce 204 from impsingle 1624. It is Step 22 in Lukasiewicz, where it appears as 'Cpp' using parenthesis-free prefix notation. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜑)
Theorem	impsingle-step25 1634	Derivation of impsingle-step25 from ax-mp 5 and impsingle 1624. It is used as a lemma in the proof of imim1 83 from impsingle 1624. It is Step 25 in Lukasiewicz, where it appears as 'CCpqCCCprqq' using parenthesis-free prefix notation. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → (((𝜑 → 𝜒) → 𝜓) → 𝜓))
Theorem	impsingle-imim1 1635	Derivation of impsingle-imim1 (imim1 83) from ax-mp 5 and impsingle 1624. It is step 29 in Lukasiewicz. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
Theorem	impsingle-peirce 1636	Derivation of impsingle-peirce (peirce 204) from ax-mp 5 and impsingle 1624. It is step 28 in Lukasiewicz. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜑)
Theorem	tarski-bernays-ax2 1637	Derivation of ax-2 7 from the Tarski-Bernays axiom set { ax-1 6, imim1 83, peirce 204 }. Note that no inference rule other than ax-mp 5 is used in this proof. This proof establishes a circle of equivalence: From { impsingle 1624 }, { ax-1 6, imim1 83, peirce 204 } was proved. From { ax-1 6, imim1 83, peirce 204 }, { ax-1 6, ax-2 7 and peirce 204 } was proved. From { ax-1 6, ax-2 7 and peirce 204 }, { impsingle 1624 } was proved. Therefore, the theorems that can be proved by selecting any one of these three distinct axiom sets must be equivalent. Prover9 and mmj2 were used to help constuct this proof. (Contributed by Larry Lesyna and Jeffrey P. Machado, 1-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
1.3.3  Derive the Lukasiewicz axioms from Meredith's sole axiom
Theorem	meredith 1638	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 1652, luk-2 1653, and luk-3 1654. Using these we finally rederive our axioms as ax1 1663, ax2 1664, and ax3 1665, 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 1639	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 1640	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 1641	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 1642	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 1643	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 1644	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 1645	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 1646	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 1647	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 1648	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 1649	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 1650	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 1651	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 1652	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 1653	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 1654	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.4  Derive the standard axioms from the Lukasiewicz axioms
Theorem	luklem1 1655	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 23-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	luklem2 1656	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → ¬ 𝜓) → (((𝜑 → 𝜒) → 𝜃) → (𝜓 → 𝜃)))
Theorem	luklem3 1657	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (((¬ 𝜑 → 𝜓) → 𝜒) → (𝜃 → 𝜒)))
Theorem	luklem4 1658	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((¬ 𝜑 → 𝜑) → 𝜑) → 𝜓) → 𝜓)
Theorem	luklem5 1659	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜑))
Theorem	luklem6 1660	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓))
Theorem	luklem7 1661	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))
Theorem	luklem8 1662	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜑) → (𝜒 → 𝜓)))
Theorem	ax1 1663	Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜑))
Theorem	ax2 1664	Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒)))
Theorem	ax3 1665	Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))
1.3.5  Derive Nicod's axiom from the standard axioms Prove Nicod's axiom and implication and negation definitions.
Theorem	nic-dfim 1666	This theorem "defines" implication in terms of 'nand'. Analogous to nanim 1487. 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 1667	This theorem "defines" negation in terms of 'nand'. Analogous to nannot 1488. 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 1668	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 1670. 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 1669	A direct proof of nic-mp 1668. (Contributed by NM, 30-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓))    ⇒   ⊢ 𝜓
Theorem	nic-ax 1670	Nicod's axiom derived from the standard ones. See Introduction to Mathematical Philosophy by B. Russell, p. 152. Like meredith 1638, the usual axioms can be derived from this and vice versa. Unlike meredith 1638, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g. { nic-ax 1670, nic-mp 1668 } is equivalent to { luk-1 1652, luk-2 1653, luk-3 1654, 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 1671	A direct proof of nic-ax 1670. (Contributed by NM, 11-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))
1.3.6  Derive the Lukasiewicz axioms from Nicod's axiom
Theorem	nic-imp 1672	Inference for nic-mp 1668 using nic-ax 1670 as major premise. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓))    ⇒   ⊢ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))
Theorem	nic-idlem1 1673	Lemma for nic-id 1675. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜃 ⊼ (𝜏 ⊼ (𝜏 ⊼ 𝜏))) ⊼ (((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ 𝜃) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ 𝜃)))
Theorem	nic-idlem2 1674	Lemma for nic-id 1675. Inference used by nic-id 1675. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜂 ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ 𝜃))    ⇒   ⊢ ((𝜃 ⊼ (𝜏 ⊼ (𝜏 ⊼ 𝜏))) ⊼ 𝜂)
Theorem	nic-id 1675	Theorem id 22 expressed with ⊼. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜏 ⊼ (𝜏 ⊼ 𝜏))
Theorem	nic-swap 1676	The connector ⊼ is symmetric. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜃 ⊼ 𝜑) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))
Theorem	nic-isw1 1677	Inference version of nic-swap 1676. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜃 ⊼ 𝜑)    ⇒   ⊢ (𝜑 ⊼ 𝜃)
Theorem	nic-isw2 1678	Inference for swapping nested terms. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜓 ⊼ (𝜃 ⊼ 𝜑))    ⇒   ⊢ (𝜓 ⊼ (𝜑 ⊼ 𝜃))
Theorem	nic-iimp1 1679	Inference version of nic-imp 1672 using right-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓))    &   ⊢ (𝜃 ⊼ 𝜒)    ⇒   ⊢ (𝜃 ⊼ 𝜑)
Theorem	nic-iimp2 1680	Inference version of nic-imp 1672 using left-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ⊼ 𝜓) ⊼ (𝜒 ⊼ 𝜒))    &   ⊢ (𝜃 ⊼ 𝜑)    ⇒   ⊢ (𝜃 ⊼ (𝜒 ⊼ 𝜒))
Theorem	nic-idel 1681	Inference to remove the trailing term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓))    ⇒   ⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜒))
Theorem	nic-ich 1682	Chained inference. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ⊼ (𝜓 ⊼ 𝜓))    &   ⊢ (𝜓 ⊼ (𝜒 ⊼ 𝜒))    ⇒   ⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜒))
Theorem	nic-idbl 1683	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 1684	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 1685 and nic-bi2 1686 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 1685	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 1686	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 1687	Derive the standard modus ponens from nic-mp 1668. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ 𝜓
Theorem	nic-luk1 1688	Proof of luk-1 1652 from nic-ax 1670 and nic-mp 1668 (and definitions nic-dfim 1666 and nic-dfneg 1667). Note that the standard axioms ax-1 6, ax-2 7, and ax-3 8 are proved from the Lukasiewicz axioms by theorems ax1 1663, ax2 1664, and ax3 1665. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
Theorem	nic-luk2 1689	Proof of luk-2 1653 from nic-ax 1670 and nic-mp 1668. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((¬ 𝜑 → 𝜑) → 𝜑)
Theorem	nic-luk3 1690	Proof of luk-3 1654 from nic-ax 1670 and nic-mp 1668. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (¬ 𝜑 → 𝜓))
1.3.7  Derive Nicod's Axiom from Lukasiewicz's First Sheffer Stroke Axiom
Theorem	lukshef-ax1 1691	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 1668 for its constructions. Here, the axiom is proved as a substitution instance of nic-ax 1670. (Contributed by Anthony Hart, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜃 ⊼ (𝜃 ⊼ 𝜃)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))
Theorem	lukshefth1 1692	Lemma for renicax 1694. (Contributed by NM, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((𝜏 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜏) ⊼ (𝜑 ⊼ 𝜏))) ⊼ (𝜃 ⊼ (𝜃 ⊼ 𝜃))) ⊼ (𝜑 ⊼ (𝜓 ⊼ 𝜒)))
Theorem	lukshefth2 1693	Lemma for renicax 1694. (Contributed by NM, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜏 ⊼ 𝜃) ⊼ ((𝜃 ⊼ 𝜏) ⊼ (𝜃 ⊼ 𝜏)))
Theorem	renicax 1694	A rederivation of nic-ax 1670 from lukshef-ax1 1691, proving that lukshef-ax1 1691 with nic-mp 1668 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.8  Derive the Lukasiewicz Axioms from the Tarski-Bernays-Wajsberg Axioms
Theorem	tbw-bijust 1695	Justification for tbw-negdf 1696. (Contributed by Anthony Hart, 15-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ↔ 𝜓) ↔ (((𝜑 → 𝜓) → ((𝜓 → 𝜑) → ⊥)) → ⊥))
Theorem	tbw-negdf 1696	The definition of negation, in terms of → and ⊥. (Contributed by Anthony Hart, 15-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((¬ 𝜑 → (𝜑 → ⊥)) → (((𝜑 → ⊥) → ¬ 𝜑) → ⊥)) → ⊥)
Theorem	tbw-ax1 1697	The first of four axioms in the Tarski-Bernays-Wajsberg system. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
Theorem	tbw-ax2 1698	The second of four axioms in the Tarski-Bernays-Wajsberg system. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜑))
Theorem	tbw-ax3 1699	The third of four axioms in the Tarski-Bernays-Wajsberg system. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜑)
Theorem	tbw-ax4 1700	The fourth of four axioms in the Tarski-Bernays-Wajsberg system. This axiom was added to the Tarski-Bernays axiom system (see tb-ax1 33726, tb-ax2 33727, and tb-ax3 33728) by Wajsberg for completeness. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊥ → 𝜑)