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	nic-idlem1 1601	Lemma for nic-id 1603. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜃 ⊼ (𝜏 ⊼ (𝜏 ⊼ 𝜏))) ⊼ (((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ 𝜃) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ 𝜃)))
Theorem	nic-idlem2 1602	Lemma for nic-id 1603. Inference used by nic-id 1603. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜂 ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ 𝜃))    ⇒   ⊢ ((𝜃 ⊼ (𝜏 ⊼ (𝜏 ⊼ 𝜏))) ⊼ 𝜂)
Theorem	nic-id 1603	Theorem id 22 expressed with ⊼. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜏 ⊼ (𝜏 ⊼ 𝜏))
Theorem	nic-swap 1604	The connector ⊼ is symmetric. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜃 ⊼ 𝜑) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))
Theorem	nic-isw1 1605	Inference version of nic-swap 1604. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜃 ⊼ 𝜑)    ⇒   ⊢ (𝜑 ⊼ 𝜃)
Theorem	nic-isw2 1606	Inference for swapping nested terms. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜓 ⊼ (𝜃 ⊼ 𝜑))    ⇒   ⊢ (𝜓 ⊼ (𝜑 ⊼ 𝜃))
Theorem	nic-iimp1 1607	Inference version of nic-imp 1600 using right-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓))    &   ⊢ (𝜃 ⊼ 𝜒)    ⇒   ⊢ (𝜃 ⊼ 𝜑)
Theorem	nic-iimp2 1608	Inference version of nic-imp 1600 using left-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ⊼ 𝜓) ⊼ (𝜒 ⊼ 𝜒))    &   ⊢ (𝜃 ⊼ 𝜑)    ⇒   ⊢ (𝜃 ⊼ (𝜒 ⊼ 𝜒))
Theorem	nic-idel 1609	Inference to remove the trailing term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓))    ⇒   ⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜒))
Theorem	nic-ich 1610	Chained inference. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 ⊼ (𝜓 ⊼ 𝜓))    &   ⊢ (𝜓 ⊼ (𝜒 ⊼ 𝜒))    ⇒   ⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜒))
Theorem	nic-idbl 1611	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 1612	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 1613 and nic-bi2 1614 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 1613	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 1614	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 1615	Derive the standard modus ponens from nic-mp 1596. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ 𝜓
Theorem	nic-luk1 1616	Proof of luk-1 1580 from nic-ax 1598 and nic-mp 1596 (and definitions nic-dfim 1594 and nic-dfneg 1595). Note that the standard axioms ax-1 6, ax-2 7, and ax-3 8 are proved from the Lukasiewicz axioms by theorems ax1 1591, ax2 1592, and ax3 1593. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
Theorem	nic-luk2 1617	Proof of luk-2 1581 from nic-ax 1598 and nic-mp 1596. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((¬ 𝜑 → 𝜑) → 𝜑)
Theorem	nic-luk3 1618	Proof of luk-3 1582 from nic-ax 1598 and nic-mp 1596. (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 1619	This alternative axiom for propositional calculus using the Sheffer Stroke was offered 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 1596 for its constructions. Here, the axiom is proved as a substitution instance of nic-ax 1598. (Contributed by Anthony Hart, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜃 ⊼ (𝜃 ⊼ 𝜃)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))
Theorem	lukshefth1 1620	Lemma for renicax 1622. (Contributed by NM, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((𝜏 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜏) ⊼ (𝜑 ⊼ 𝜏))) ⊼ (𝜃 ⊼ (𝜃 ⊼ 𝜃))) ⊼ (𝜑 ⊼ (𝜓 ⊼ 𝜒)))
Theorem	lukshefth2 1621	Lemma for renicax 1622. (Contributed by NM, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜏 ⊼ 𝜃) ⊼ ((𝜃 ⊼ 𝜏) ⊼ (𝜃 ⊼ 𝜏)))
Theorem	renicax 1622	A rederivation of nic-ax 1598 from lukshef-ax1 1619, proving that lukshef-ax1 1619 with nic-mp 1596 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 1623	Justification for tbw-negdf 1624. (Contributed by Anthony Hart, 15-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ↔ 𝜓) ↔ (((𝜑 → 𝜓) → ((𝜓 → 𝜑) → ⊥)) → ⊥))
Theorem	tbw-negdf 1624	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 1625	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 1626	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 1627	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 1628	The fourth of four axioms in the Tarski-Bernays-Wajsberg system. This axiom was added to the Tarski-Bernays axiom system (see tb-ax1 32378, tb-ax2 32379, and tb-ax3 32380) by Wajsberg for completeness. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊥ → 𝜑)
Theorem	tbwsyl 1629	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 1630	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 1631	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 1632	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 1633	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 1634	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 1635	luk-1 1580 derived from the Tarski-Bernays-Wajsberg axioms. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
Theorem	re1luk2 1636	luk-2 1581 derived from the Tarski-Bernays-Wajsberg axioms. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((¬ 𝜑 → 𝜑) → 𝜑)
Theorem	re1luk3 1637	luk-3 1582 derived from the Tarski-Bernays-Wajsberg axioms. This theorem, along with re1luk1 1635 and re1luk2 1636 proves that tbw-ax1 1625, tbw-ax2 1626, tbw-ax3 1627, and tbw-ax4 1628, 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.8  Derive the Tarski-Bernays-Wajsberg axioms from Meredith's First CO Axiom
Theorem	merco1 1638	A single axiom for propositional calculus offered by Meredith. This axiom is worthy of note, due to it having only 19 symbols, not counting parentheses. The more well-known meredith 1566 has 21 symbols, sans parentheses. See merco2 1661 for another axiom of equal length. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((((𝜑 → 𝜓) → (𝜒 → ⊥)) → 𝜃) → 𝜏) → ((𝜏 → 𝜑) → (𝜒 → 𝜑)))
Theorem	merco1lem1 1639	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1638. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (⊥ → 𝜒))
Theorem	retbwax4 1640	tbw-ax4 1628 rederived from merco1 1638. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (⊥ → 𝜑)
Theorem	retbwax2 1641	tbw-ax2 1626 rederived from merco1 1638. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜑))
Theorem	merco1lem2 1642	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1638. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜒) → (((𝜓 → 𝜏) → (𝜑 → ⊥)) → 𝜒))
Theorem	merco1lem3 1643	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1638. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → (𝜒 → ⊥)) → (𝜒 → 𝜑))
Theorem	merco1lem4 1644	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1638. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒))
Theorem	merco1lem5 1645	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1638. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((𝜑 → ⊥) → 𝜒) → 𝜏) → (𝜑 → 𝜏))
Theorem	merco1lem6 1646	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1638. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜒 → (𝜑 → 𝜓)))
Theorem	merco1lem7 1647	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1638. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (((𝜓 → 𝜒) → 𝜓) → 𝜓))
Theorem	retbwax3 1648	tbw-ax3 1627 rederived from merco1 1638. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜑)
Theorem	merco1lem8 1649	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1638. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ((𝜓 → (𝜓 → 𝜒)) → (𝜓 → 𝜒)))
Theorem	merco1lem9 1650	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1638. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓))
Theorem	merco1lem10 1651	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1638. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((((𝜑 → 𝜓) → 𝜒) → (𝜏 → 𝜒)) → 𝜑) → (𝜃 → 𝜑))
Theorem	merco1lem11 1652	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1638. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → (((𝜒 → (𝜑 → 𝜏)) → ⊥) → 𝜓))
Theorem	merco1lem12 1653	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1638. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → (((𝜒 → (𝜑 → 𝜏)) → 𝜑) → 𝜓))
Theorem	merco1lem13 1654	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1638. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((𝜑 → 𝜓) → (𝜒 → 𝜓)) → 𝜏) → (𝜑 → 𝜏))
Theorem	merco1lem14 1655	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1638. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((𝜑 → 𝜓) → 𝜓) → 𝜒) → (𝜑 → 𝜒))
Theorem	merco1lem15 1656	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1638. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → (𝜑 → (𝜒 → 𝜓)))
Theorem	merco1lem16 1657	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1638. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → (𝜓 → 𝜒)) → 𝜏) → ((𝜑 → 𝜒) → 𝜏))
Theorem	merco1lem17 1658	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1638. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((((𝜑 → 𝜓) → 𝜑) → 𝜒) → 𝜏) → ((𝜑 → 𝜒) → 𝜏))
Theorem	merco1lem18 1659	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1638. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜓 → 𝜑) → (𝜓 → 𝜒)))
Theorem	retbwax1 1660	tbw-ax1 1625 rederived from merco1 1638. This theorem, along with retbwax2 1641, retbwax3 1648, and retbwax4 1640, shows that merco1 1638 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.9  Derive the Tarski-Bernays-Wajsberg axioms from Meredith's Second CO Axiom
Theorem	merco2 1661	A single axiom for propositional calculus offered by Meredith. This axiom has 19 symbols, sans auxiliaries. See notes in merco1 1638. (Contributed by Anthony Hart, 7-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → ((⊥ → 𝜒) → 𝜃)) → ((𝜃 → 𝜑) → (𝜏 → (𝜂 → 𝜑))))
Theorem	mercolem1 1662	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2 1661. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜓 → (𝜃 → 𝜒)))
Theorem	mercolem2 1663	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2 1661. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜑) → (𝜒 → (𝜃 → 𝜑)))
Theorem	mercolem3 1664	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2 1661. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜓 → 𝜒) → (𝜓 → (𝜑 → 𝜒)))
Theorem	mercolem4 1665	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2 1661. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜃 → (𝜂 → 𝜑)) → (((𝜃 → 𝜒) → 𝜑) → (𝜏 → (𝜂 → 𝜑))))
Theorem	mercolem5 1666	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2 1661. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜃 → ((𝜃 → 𝜑) → (𝜏 → (𝜒 → 𝜑))))
Theorem	mercolem6 1667	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2 1661. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → (𝜓 → (𝜑 → 𝜒))) → (𝜓 → (𝜑 → 𝜒)))
Theorem	mercolem7 1668	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2 1661. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → (((𝜑 → 𝜒) → (𝜃 → 𝜓)) → (𝜃 → 𝜓)))
Theorem	mercolem8 1669	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2 1661. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜓 → (𝜑 → 𝜒)) → (𝜏 → (𝜃 → (𝜑 → 𝜒)))))
Theorem	re1tbw1 1670	tbw-ax1 1625 rederived from merco2 1661. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
Theorem	re1tbw2 1671	tbw-ax2 1626 rederived from merco2 1661. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜑))
Theorem	re1tbw3 1672	tbw-ax3 1627 rederived from merco2 1661. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜑)
Theorem	re1tbw4 1673	tbw-ax4 1628 rederived from merco2 1661. This theorem, along with re1tbw1 1670, re1tbw2 1671, and re1tbw3 1672, shows that merco2 1661, 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.10  Derive the Lukasiewicz axioms from the Russell-Bernays Axioms
Theorem	rb-bijust 1674	Justification for rb-imdf 1675. (Contributed by Anthony Hart, 17-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ↔ 𝜓) ↔ ¬ (¬ (¬ 𝜑 ∨ 𝜓) ∨ ¬ (¬ 𝜓 ∨ 𝜑)))
Theorem	rb-imdf 1675	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 1676	Modus ponens for ∨ ¬ axiom systems. (Contributed by Anthony Hart, 12-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (¬ 𝜑 ∨ 𝜓)    ⇒   ⊢ 𝜓
Theorem	rb-ax1 1677	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 1678	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 1679	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 1680	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 1681	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 1682	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 1683	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 1684	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 1685	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 1686	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 1687	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 1688	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 1689	ax-mp 5 derived from Russell-Bernays'. (Contributed by Anthony Hart, 19-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ 𝜓
Theorem	re2luk1 1690	luk-1 1580 derived from Russell-Bernays'. (Contributed by Anthony Hart, 19-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒)))
Theorem	re2luk2 1691	luk-2 1581 derived from Russell-Bernays'. (Contributed by Anthony Hart, 19-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((¬ 𝜑 → 𝜑) → 𝜑)
Theorem	re2luk3 1692	luk-3 1582 derived from Russell-Bernays'. This theorem, along with re1axmp 1689, re2luk1 1690, and re2luk2 1691 shows that rb-ax1 1677, rb-ax2 1678, rb-ax3 1679, and rb-ax4 1680, along with anmp 1676, 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.)
⊢ (𝜑 → (¬ 𝜑 → 𝜓))
1.3.11  Stoic logic non-modal portion (Chrysippus of Soli) The Greek Stoics developed a system of logic called Stoic logic. The Stoic Chrysippus, in particular, was often considered one of the greatest logicians of antiquity. Stoic logic is different from Aristotle's system, since it focuses on propositional logic, though later thinkers did combine the systems of the Stoics with Aristotle. Jan Lukasiewicz reports, "For anybody familiar with mathematical logic it is self-evident that the Stoic dialectic is the ancient form of modern propositional logic" ( On the history of the logic of proposition by Jan Lukasiewicz (1934), translated in: Selected Works - Edited by Ludwik Borkowski - Amsterdam, North-Holland, 1970 pp. 197-217, referenced in "History of Logic" https://www.historyoflogic.com/logic-stoics.htm). In this section we show that the propositional logic system we use (which is non-modal) is at least as strong as the non-modal portion of Stoic logic. We show this by showing that our system assumes or proves all of key features of Stoic logic's non-modal portion (specifically the Stoic logic indemonstrables, themata, and principles). "In terms of contemporary logic, Stoic syllogistic is best understood as a substructural backwards-working Gentzen-style natural-deduction system that consists of five kinds of axiomatic arguments (the indemonstrables) and four inference rules, called themata. An argument is a syllogism precisely if it either is an indemonstrable or can be reduced to one by means of the themata (Diogenes Laertius (D. L. 7.78))." (Ancient Logic, Stanford Encyclopedia of Philosophy https://plato.stanford.edu/entries/logic-ancient/). There are also a few "principles" that support logical reasoning, discussed below. For more information, see "Stoic Logic" by Susanne Bobzien, especially [Bobzien] p. 110-120, especially for a discussion about the themata (including how they were reconstructed and how they were used). There are differences in the systems we can only partly represent, for example, in Stoic logic "truth and falsehood are temporal properties of assertibles... They can belong to an assertible at one time but not at another" ([Bobzien] p. 87). Stoic logic also included various kinds of modalities, which we do not include here since our basic propositional logic does not include modalities. A key part of the Stoic logic system is a set of five "indemonstrables" assigned to Chrysippus of Soli by Diogenes Laertius, though in general it is difficult to assign specific ideas to specific thinkers. The indemonstrables are described in, for example, [Lopez-Astorga] p. 11 , [Sanford] p. 39, and [Hitchcock] p. 5. These indemonstrables are modus ponendo ponens (modus ponens) ax-mp 5, modus tollendo tollens (modus tollens) mto 188, modus ponendo tollens I mptnan 1693, modus ponendo tollens II mptxor 1694, and modus tollendo ponens (exclusive-or version) mtpxor 1696. The first is an axiom, the second is already proved; in this section we prove the other three. Note that modus tollendo ponens mtpxor 1696 originally used exclusive-or, but over time the name modus tollendo ponens has increasingly referred to an inclusive-or variation, which is proved in mtpor 1695. After we prove the indemonstratables, we then prove all the Stoic logic themata (the inference rules of Stoic logic; "thema" is singular). This is straightforward for thema 1 (stoic1a 1697 and stoic1b 1698) and thema 3 (stoic3 1701). However, while Stoic logic was once a leading logic system, most direct information about Stoic logic has since been lost, including the exact texts of thema 2 and thema 4. There are, however, enough references and specific examples to support reconstruction. Themata 2 and 4 have been reconstructed; see statements T2 and T4 in [Bobzien] p. 110-120 and our proofs of them in stoic2a 1699, stoic2b 1700, stoic4a 1702, and stoic4b 1703. Stoic logic also had a set of principles involving assertibles. Statements in [Bobzien] p. 99 express the known principles. The following paragraphs discuss these principles and our proofs of them. "A principle of double negation, expressed by saying that a double-negation (Not: not: p) is equivalent to the assertible that is doubly negated (p) (DL VII 69)." In other words, (𝜑 ↔ ¬ ¬ 𝜑) as proven in notnotb 304. "The principle that all conditionals that are formed by using the same assertible twice (like 'If p, p') are true (Cic. Acad. II 98)." In other words, (𝜑 → 𝜑) as proven in id 22. "The principle that all disjunctions formed by a contradiction (like 'Either p or not: p') are true (S. E. M VIII 282)". Remember that in Stoic logic, 'or' means 'exclusive or'. In other words, (𝜑 ⊻ ¬ 𝜑) as proven in xorexmid 1480. [Bobzien] p. 99 also suggests that Stoic logic may have dealt with commutativity (see xorcom 1467 and ancom 466) and the principle of contraposition (con4 112) (pointing to DL VII 194). In short, the non-modal propositional logic system we use is at least as strong as the non-modal portion of Stoic logic. For more about Aristotle's system, see barbara 2563 and related theorems.
Theorem	mptnan 1693	Modus ponendo tollens 1, one of the "indemonstrables" in Stoic logic. See rule 1 on [Lopez-Astorga] p. 12 , rule 1 on [Sanford] p. 40, and rule A3 in [Hitchcock] p. 5. Sanford describes this rule second (after mptxor 1694) as a "safer, and these days much more common" version of modus ponendo tollens because it avoids confusion between inclusive-or and exclusive-or. (Contributed by David A. Wheeler, 3-Jul-2016.)
⊢ 𝜑    &   ⊢ ¬ (𝜑 ∧ 𝜓)    ⇒   ⊢ ¬ 𝜓
Theorem	mptxor 1694	Modus ponendo tollens 2, one of the "indemonstrables" in Stoic logic. Note that this uses exclusive-or ⊻. See rule 2 on [Lopez-Astorga] p. 12 , rule 4 on [Sanford] p. 39 and rule A4 in [Hitchcock] p. 5 . (Contributed by David A. Wheeler, 3-Jul-2016.) (Proof shortened by Wolf Lammen, 12-Nov-2017.) (Proof shortened by BJ, 19-Apr-2019.)
⊢ 𝜑    &   ⊢ (𝜑 ⊻ 𝜓)    ⇒   ⊢ ¬ 𝜓
Theorem	mtpor 1695	Modus tollendo ponens (inclusive-or version), aka disjunctive syllogism. This is similar to mtpxor 1696, one of the five original "indemonstrables" in Stoic logic. However, in Stoic logic this rule used exclusive-or, while the name modus tollendo ponens often refers to a variant of the rule that uses inclusive-or instead. The rule says, "if 𝜑 is not true, and 𝜑 or 𝜓 (or both) are true, then 𝜓 must be true." An alternative phrasing is, "Once you eliminate the impossible, whatever remains, no matter how improbable, must be the truth." -- Sherlock Holmes (Sir Arthur Conan Doyle, 1890: The Sign of the Four, ch. 6). (Contributed by David A. Wheeler, 3-Jul-2016.) (Proof shortened by Wolf Lammen, 11-Nov-2017.)
⊢ ¬ 𝜑    &   ⊢ (𝜑 ∨ 𝜓)    ⇒   ⊢ 𝜓
Theorem	mtpxor 1696	Modus tollendo ponens (original exclusive-or version), aka disjunctive syllogism, similar to mtpor 1695, one of the five "indemonstrables" in Stoic logic. The rule says, "if 𝜑 is not true, and either 𝜑 or 𝜓 (exclusively) are true, then 𝜓 must be true." Today the name "modus tollendo ponens" often refers to a variant, the inclusive-or version as defined in mtpor 1695. See rule 3 on [Lopez-Astorga] p. 12 (note that the "or" is the same as mptxor 1694, that is, it is exclusive-or df-xor 1465), rule 3 of [Sanford] p. 39 (where it is not as clearly stated which kind of "or" is used but it appears to be in the same sense as mptxor 1694), and rule A5 in [Hitchcock] p. 5 (exclusive-or is expressly used). (Contributed by David A. Wheeler, 4-Jul-2016.) (Proof shortened by Wolf Lammen, 11-Nov-2017.) (Proof shortened by BJ, 19-Apr-2019.)
⊢ ¬ 𝜑    &   ⊢ (𝜑 ⊻ 𝜓)    ⇒   ⊢ 𝜓
Theorem	stoic1a 1697	Stoic logic Thema 1 (part a). The first thema of the four Stoic logic themata, in its basic form, was: "When from two (assertibles) a third follows, then from either of them together with the contradictory of the conclusion the contradictory of the other follows." (Apuleius Int. 209.9-14), see [Bobzien] p. 117 and https://plato.stanford.edu/entries/logic-ancient/ We will represent thema 1 as two very similar rules stoic1a 1697 and stoic1b 1698 to represent each side. (Contributed by David A. Wheeler, 16-Feb-2019.) (Proof shortened by Wolf Lammen, 21-May-2020.)
⊢ ((𝜑 ∧ 𝜓) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ ¬ 𝜃) → ¬ 𝜓)
Theorem	stoic1b 1698	Stoic logic Thema 1 (part b). The other part of thema 1 of Stoic logic; see stoic1a 1697. (Contributed by David A. Wheeler, 16-Feb-2019.)
⊢ ((𝜑 ∧ 𝜓) → 𝜃)    ⇒   ⊢ ((𝜓 ∧ ¬ 𝜃) → ¬ 𝜑)
Theorem	stoic2a 1699	Stoic logic Thema 2 version a. Statement T2 of [Bobzien] p. 117 shows a reconstructed version of Stoic logic thema 2 as follows: "When from two assertibles a third follows, and from the third and one (or both) of the two another follows, then this other follows from the first two." Bobzien uses constructs such as 𝜑, 𝜓⊢ 𝜒; in Metamath we will represent that construct as 𝜑 ∧ 𝜓 → 𝜒. This version a is without the phrase "or both"; see stoic2b 1700 for the version with the phrase "or both". We already have this rule as syldan 487, so here we show the equivalence and discourage its use. (New usage is discouraged.) (Contributed by David A. Wheeler, 17-Feb-2019.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
Theorem	stoic2b 1700	Stoic logic Thema 2 version b. See stoic2a 1699. Version b is with the phrase "or both". We already have this rule as mpd3an3 1425, so here we prove the equivalence and discourage its use. (New usage is discouraged.) (Contributed by David A. Wheeler, 17-Feb-2019.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜃)