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	ax3 1701	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 1702	This theorem "defines" implication in terms of 'nand'. Analogous to nanim 1528. 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 1703	This theorem "defines" negation in terms of 'nand'. Analogous to nannot 1529. 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 1704	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 1706. 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 1705	A direct proof of nic-mp 1704. (Contributed by NM, 30-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓))    ⇒   ⊢ 𝜓
Theorem	nic-ax 1706	Nicod's axiom derived from the standard ones. See Introduction to Mathematical Philosophy by B. Russell, p. 152. Like meredith 1674, the usual axioms can be derived from this and vice versa. Unlike meredith 1674, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g., { nic-ax 1706, nic-mp 1704 } is equivalent to { luk-1 1688, luk-2 1689, luk-3 1690, 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 1707	A direct proof of nic-ax 1706. (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 1708	Inference for nic-mp 1704 using nic-ax 1706 as major premise. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓))    ⇒   ⊢ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))
Theorem	nic-idlem1 1709	Lemma for nic-id 1711. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜃 ⊼ (𝜏 ⊼ (𝜏 ⊼ 𝜏))) ⊼ (((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ 𝜃) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ 𝜃)))
Theorem	nic-idlem2 1710	Lemma for nic-id 1711. Inference used by nic-id 1711. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜂 ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ 𝜃))    ⇒   ⊢ ((𝜃 ⊼ (𝜏 ⊼ (𝜏 ⊼ 𝜏))) ⊼ 𝜂)
Theorem	nic-id 1711	Theorem id 23 expressed with ⊼. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜏 ⊼ (𝜏 ⊼ 𝜏))
Theorem	nic-swap 1712	The connector ⊼ is symmetric. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜃 ⊼ 𝜑) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))
Theorem	nic-isw1 1713	Inference version of nic-swap 1712. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜃 ⊼ 𝜑)    ⇒   ⊢ (𝜑 ⊼ 𝜃)
Theorem	nic-isw2 1714	Inference for swapping nested terms. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜓 ⊼ (𝜃 ⊼ 𝜑))    ⇒   ⊢ (𝜓 ⊼ (𝜑 ⊼ 𝜃))
Theorem	nic-iimp1 1715	Inference version of nic-imp 1708 using right-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓))    &   ⊢ (𝜃 ⊼ 𝜒)    ⇒   ⊢ (𝜃 ⊼ 𝜑)
Theorem	nic-iimp2 1716	Inference version of nic-imp 1708 using left-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ⊼ 𝜓) ⊼ (𝜒 ⊼ 𝜒))    &   ⊢ (𝜃 ⊼ 𝜑)    ⇒   ⊢ (𝜃 ⊼ (𝜒 ⊼ 𝜒))
Theorem	nic-idel 1717	Inference to remove the trailing term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓))    ⇒   ⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜒))
Theorem	nic-ich 1718	Chained inference. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ⊼ (𝜓 ⊼ 𝜓))    &   ⊢ (𝜓 ⊼ (𝜒 ⊼ 𝜒))    ⇒   ⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜒))
Theorem	nic-idbl 1719	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 1720	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 1721 and nic-bi2 1722 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 1721	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 1722	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 1723	Derive the standard modus ponens from nic-mp 1704. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ 𝜓
Theorem	nic-luk1 1724	Proof of luk-1 1688 from nic-ax 1706 and nic-mp 1704 (and Definitions nic-dfim 1702 and nic-dfneg 1703). Note that the standard axioms ax-1 6, ax-2 7, and ax-3 8 are proved from the Lukasiewicz axioms by Theorems ax1 1699, ax2 1700, and ax3 1701. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
Theorem	nic-luk2 1725	Proof of luk-2 1689 from nic-ax 1706 and nic-mp 1704. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((¬ 𝜑 → 𝜑) → 𝜑)
Theorem	nic-luk3 1726	Proof of luk-3 1690 from nic-ax 1706 and nic-mp 1704. (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 1727	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 1704 for its constructions. Here, the axiom is proved as a substitution instance of nic-ax 1706. (Contributed by Anthony Hart, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜃 ⊼ (𝜃 ⊼ 𝜃)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))
Theorem	lukshefth1 1728	Lemma for renicax 1730. (Contributed by NM, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((𝜏 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜏) ⊼ (𝜑 ⊼ 𝜏))) ⊼ (𝜃 ⊼ (𝜃 ⊼ 𝜃))) ⊼ (𝜑 ⊼ (𝜓 ⊼ 𝜒)))
Theorem	lukshefth2 1729	Lemma for renicax 1730. (Contributed by NM, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜏 ⊼ 𝜃) ⊼ ((𝜃 ⊼ 𝜏) ⊼ (𝜃 ⊼ 𝜏)))
Theorem	renicax 1730	A rederivation of nic-ax 1706 from lukshef-ax1 1727, proving that lukshef-ax1 1727 with nic-mp 1704 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 1731	Justification for tbw-negdf 1732. (Contributed by Anthony Hart, 15-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ↔ 𝜓) ↔ (((𝜑 → 𝜓) → ((𝜓 → 𝜑) → ⊥)) → ⊥))
Theorem	tbw-negdf 1732	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 1733	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 1734	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 1735	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 1736	The fourth of four axioms in the Tarski-Bernays-Wajsberg system. This axiom was added to the Tarski-Bernays axiom system (see tb-ax1 36934, tb-ax2 36935, and tb-ax3 36936) by Wajsberg for completeness. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊥ → 𝜑)
Theorem	tbwsyl 1737	Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	tbwlem1 1738	Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))
Theorem	tbwlem2 1739	Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → ⊥)) → (((𝜑 → 𝜒) → 𝜃) → (𝜓 → 𝜃)))
Theorem	tbwlem3 1740	Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((((𝜑 → ⊥) → 𝜑) → 𝜑) → 𝜓) → 𝜓)
Theorem	tbwlem4 1741	Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → ⊥) → 𝜓) → ((𝜓 → ⊥) → 𝜑))
Theorem	tbwlem5 1742	Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → (𝜓 → ⊥)) → ⊥) → 𝜑)
Theorem	re1luk1 1743	luk-1 1688 derived from the Tarski-Bernays-Wajsberg axioms. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
Theorem	re1luk2 1744	luk-2 1689 derived from the Tarski-Bernays-Wajsberg axioms. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((¬ 𝜑 → 𝜑) → 𝜑)
Theorem	re1luk3 1745	luk-3 1690 derived from the Tarski-Bernays-Wajsberg axioms. This theorem, along with re1luk1 1743 and re1luk2 1744 proves that tbw-ax1 1733, tbw-ax2 1734, tbw-ax3 1735, and tbw-ax4 1736, with ax-mp 5 can be used as a complete axiom system for all of propositional calculus. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (¬ 𝜑 → 𝜓))
1.3.9  Derive the Tarski-Bernays-Wajsberg axioms from Meredith's First CO Axiom
Theorem	merco1 1746	A single axiom for propositional calculus discovered by C. A. Meredith. This axiom is worthy of note, due to it having only 19 symbols, not counting parentheses. The more well-known meredith 1674 has 21 symbols, sans parentheses. See merco2 1769 for another axiom of equal length. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((𝜏 → 𝜑) → (𝜒 → 𝜑)))
Theorem	merco1lem1 1747	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1746. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (⊥ → 𝜒))
Theorem	retbwax4 1748	tbw-ax4 1736 rederived from merco1 1746. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊥ → 𝜑)
Theorem	retbwax2 1749	tbw-ax2 1734 rederived from merco1 1746. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜑))
Theorem	merco1lem2 1750	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1746. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜒) → (((𝜓 → 𝜏) → (𝜑 → ⊥)) → 𝜒))
Theorem	merco1lem3 1751	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1746. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → (𝜒 → ⊥)) → (𝜒 → 𝜑))
Theorem	merco1lem4 1752	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1746. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒))
Theorem	merco1lem5 1753	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1746. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((𝜑 → ⊥) → 𝜒) → 𝜏) → (𝜑 → 𝜏))
Theorem	merco1lem6 1754	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1746. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜒 → (𝜑 → 𝜓)))
Theorem	merco1lem7 1755	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1746. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (((𝜓 → 𝜒) → 𝜓) → 𝜓))
Theorem	retbwax3 1756	tbw-ax3 1735 rederived from merco1 1746. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜑)
Theorem	merco1lem8 1757	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1746. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ((𝜓 → (𝜓 → 𝜒)) → (𝜓 → 𝜒)))
Theorem	merco1lem9 1758	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1746. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓))
Theorem	merco1lem10 1759	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1746. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((((𝜑 → 𝜓) → 𝜒) → (𝜏 → 𝜒)) → 𝜑) → (𝜃 → 𝜑))
Theorem	merco1lem11 1760	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1746. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → (((𝜒 → (𝜑 → 𝜏)) → ⊥) → 𝜓))
Theorem	merco1lem12 1761	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1746. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → (((𝜒 → (𝜑 → 𝜏)) → 𝜑) → 𝜓))
Theorem	merco1lem13 1762	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1746. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((𝜑 → 𝜓) → (𝜒 → 𝜓)) → 𝜏) → (𝜑 → 𝜏))
Theorem	merco1lem14 1763	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1746. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((𝜑 → 𝜓) → 𝜓) → 𝜒) → (𝜑 → 𝜒))
Theorem	merco1lem15 1764	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1746. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → (𝜑 → (𝜒 → 𝜓)))
Theorem	merco1lem16 1765	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1746. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → (𝜓 → 𝜒)) → 𝜏) → ((𝜑 → 𝜒) → 𝜏))
Theorem	merco1lem17 1766	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1746. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((((𝜑 → 𝜓) → 𝜑) → 𝜒) → 𝜏) → ((𝜑 → 𝜒) → 𝜏))
Theorem	merco1lem18 1767	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1746. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜓 → 𝜑) → (𝜓 → 𝜒)))
Theorem	retbwax1 1768	tbw-ax1 1733 rederived from merco1 1746. This theorem, along with retbwax2 1749, retbwax3 1756, and retbwax4 1748, shows that merco1 1746 with ax-mp 5 can be used as a complete axiomatization of propositional calculus. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
1.3.10  Derive the Tarski-Bernays-Wajsberg axioms from Meredith's Second CO Axiom
Theorem	merco2 1769	A single axiom for propositional calculus discovered by C. A. Meredith. This axiom has 19 symbols, sans auxiliaries. See notes in merco1 1746. (Contributed by Anthony Hart, 7-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → ((⊥ → 𝜒) → 𝜃)) → ((𝜃 → 𝜑) → (𝜏 → (𝜂 → 𝜑))))
Theorem	mercolem1 1770	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2 1769. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜓 → (𝜃 → 𝜒)))
Theorem	mercolem2 1771	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2 1769. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜑) → (𝜒 → (𝜃 → 𝜑)))
Theorem	mercolem3 1772	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2 1769. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜓 → 𝜒) → (𝜓 → (𝜑 → 𝜒)))
Theorem	mercolem4 1773	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2 1769. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑))))
Theorem	mercolem5 1774	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2 1769. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜃 → ((𝜃 → 𝜑) → (𝜏 → (𝜒 → 𝜑))))
Theorem	mercolem6 1775	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2 1769. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → (𝜑 → 𝜒))) → (𝜓 → (𝜑 → 𝜒)))
Theorem	mercolem7 1776	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2 1769. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → (((𝜑 → 𝜒) → (𝜃 → 𝜓)) → (𝜃 → 𝜓)))
Theorem	mercolem8 1777	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2 1769. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜓 → (𝜑 → 𝜒)) → (𝜏 → (𝜃 → (𝜑 → 𝜒)))))
Theorem	re1tbw1 1778	tbw-ax1 1733 rederived from merco2 1769. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
Theorem	re1tbw2 1779	tbw-ax2 1734 rederived from merco2 1769. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜑))
Theorem	re1tbw3 1780	tbw-ax3 1735 rederived from merco2 1769. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜑)
Theorem	re1tbw4 1781	tbw-ax4 1736 rederived from merco2 1769. This theorem, along with re1tbw1 1778, re1tbw2 1779, and re1tbw3 1780, shows that merco2 1769, along with ax-mp 5, can be used as a complete axiomatization of propositional calculus. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊥ → 𝜑)
1.3.11  Derive the Lukasiewicz axioms from the Russell-Bernays Axioms
Theorem	rb-bijust 1782	Justification for rb-imdf 1783. (Contributed by Anthony Hart, 17-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ↔ 𝜓) ↔ ¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ (¬ 𝜓 ∨ 𝜑)))
Theorem	rb-imdf 1783	The definition of implication, in terms of ∨ and ¬. (Contributed by Anthony Hart, 17-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ (¬ (¬ (𝜑 → 𝜓) ∨ (¬ 𝜑 ∨ 𝜓)) ∨ ¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ (𝜑 → 𝜓)))
Theorem	anmp 1784	Modus ponens for { ∨ , ¬ } axiom systems. (Contributed by Anthony Hart, 12-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (¬ 𝜑 ∨ 𝜓)    ⇒   ⊢ 𝜓
Theorem	rb-ax1 1785	The first of four axioms in the Russell-Bernays axiom system. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ (¬ 𝜓 ∨ 𝜒) ∨ (¬ (𝜑 ∨ 𝜓) ∨ (𝜑 ∨ 𝜒)))
Theorem	rb-ax2 1786	The second of four axioms in the Russell-Bernays axiom system. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ (𝜑 ∨ 𝜓) ∨ (𝜓 ∨ 𝜑))
Theorem	rb-ax3 1787	The third of four axioms in the Russell-Bernays axiom system. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝜑 ∨ (𝜓 ∨ 𝜑))
Theorem	rb-ax4 1788	The fourth of four axioms in the Russell-Bernays axiom system. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ (𝜑 ∨ 𝜑) ∨ 𝜑)
Theorem	rbsyl 1789	Used to rederive the Lukasiewicz axioms from Russell-Bernays'. (Contributed by Anthony Hart, 18-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝜓 ∨ 𝜒)    &   ⊢ (𝜑 ∨ 𝜓)    ⇒   ⊢ (𝜑 ∨ 𝜒)
Theorem	rblem1 1790	Used to rederive the Lukasiewicz axioms from Russell-Bernays'. (Contributed by Anthony Hart, 18-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝜑 ∨ 𝜓)    &   ⊢ (¬ 𝜒 ∨ 𝜃)    ⇒   ⊢ (¬ (𝜑 ∨ 𝜒) ∨ (𝜓 ∨ 𝜃))
Theorem	rblem2 1791	Used to rederive the Lukasiewicz axioms from Russell-Bernays'. (Contributed by Anthony Hart, 18-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ (𝜒 ∨ 𝜑) ∨ (𝜒 ∨ (𝜑 ∨ 𝜓)))
Theorem	rblem3 1792	Used to rederive the Lukasiewicz axioms from Russell-Bernays'. (Contributed by Anthony Hart, 18-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ (𝜒 ∨ 𝜑) ∨ ((𝜒 ∨ 𝜓) ∨ 𝜑))
Theorem	rblem4 1793	Used to rederive the Lukasiewicz axioms from Russell-Bernays'. (Contributed by Anthony Hart, 18-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝜑 ∨ 𝜃)    &   ⊢ (¬ 𝜓 ∨ 𝜏)    &   ⊢ (¬ 𝜒 ∨ 𝜂)    ⇒   ⊢ (¬ ((𝜑 ∨ 𝜓) ∨ 𝜒) ∨ ((𝜂 ∨ 𝜏) ∨ 𝜃))
Theorem	rblem5 1794	Used to rederive the Lukasiewicz axioms from Russell-Bernays'. (Contributed by Anthony Hart, 19-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ (¬ ¬ 𝜑 ∨ 𝜓) ∨ (¬ ¬ 𝜓 ∨ 𝜑))
Theorem	rblem6 1795	Used to rederive the Lukasiewicz axioms from Russell-Bernays'. (Contributed by Anthony Hart, 19-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ (¬ 𝜓 ∨ 𝜑))    ⇒   ⊢ (¬ 𝜑 ∨ 𝜓)
Theorem	rblem7 1796	Used to rederive the Lukasiewicz axioms from Russell-Bernays'. (Contributed by Anthony Hart, 19-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ (¬ 𝜓 ∨ 𝜑))    ⇒   ⊢ (¬ 𝜓 ∨ 𝜑)
Theorem	re1axmp 1797	ax-mp 5 derived from Russell-Bernays'. (Contributed by Anthony Hart, 19-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ 𝜓
Theorem	re2luk1 1798	luk-1 1688 derived from Russell-Bernays'. (Contributed by Anthony Hart, 19-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
Theorem	re2luk2 1799	luk-2 1689 derived from Russell-Bernays'. (Contributed by Anthony Hart, 19-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((¬ 𝜑 → 𝜑) → 𝜑)
Theorem	re2luk3 1800	luk-3 1690 derived from Russell-Bernays'. This theorem, along with re1axmp 1797, re2luk1 1798, and re2luk2 1799 shows that rb-ax1 1785, rb-ax2 1786, rb-ax3 1787, and rb-ax4 1788, along with anmp 1784, can be used as a complete axiomatization of propositional calculus. (Contributed by Anthony Hart, 19-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (¬ 𝜑 → 𝜓))