P. 15 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 1401-1500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cadtru 1401	Rotation law for adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ cadd( ⊤ , ⊤ , φ)
Theorem	had1 1402	If the first parameter is true, the half adder is equivalent to the equality of the other two inputs. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ (φ → (hadd(φ, ψ, χ) ↔ (ψ ↔ χ)))
Theorem	had0 1403	If the first parameter is false, the half adder is equivalent to the XOR of the other two inputs. (Contributed by Mario Carneiro, 4-Sep-2016.)
⊢ (¬ φ → (hadd(φ, ψ, χ) ↔ (ψ ⊻ χ)))
1.3  Other axiomatizations of classical propositional calculus
1.3.1  Derive the Lukasiewicz axioms from Meredith's sole axiom
Theorem	meredith 1404	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 1420, luk-2 1421, and luk-3 1422. Using these we finally re-derive our axioms as ax1 1431, ax2 1432, and ax3 1433, 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	axmeredith 1405	Alias for meredith 1404 which "verify markup *" will match to ax-meredith 1406. (Contributed by NM, 21-Aug-2017.) (New usage is discouraged.)
⊢ (((((φ → ψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((τ → φ) → (θ → φ)))
Axiom	ax-meredith 1406	Theorem meredith 1404 restated as an axiom. This will allow us to ensure that the rederivation of ax1 1431, ax2 1432, and ax3 1433 below depend only on Meredith's sole axiom and not accidentally on a previous theorem above. Outside of this section, we will not make use of this axiom. (Contributed by NM, 14-Dec-2002.) (New usage is discouraged.)
⊢ (((((φ → ψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((τ → φ) → (θ → φ)))
Theorem	merlem1 1407	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 1408	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 1409	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 1410	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 1411	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 1412	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 1413	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 1414	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 1415	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 1416	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 1417	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 1418	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 1419	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 1420	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 1421	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 1422	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.2  Derive the standard axioms from the Lukasiewicz axioms
Theorem	luklem1 1423	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 23-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (φ → ψ)    &   ⊢ (ψ → χ)    ⇒   ⊢ (φ → χ)
Theorem	luklem2 1424	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((φ → ¬ ψ) → (((φ → χ) → θ) → (ψ → θ)))
Theorem	luklem3 1425	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (φ → (((¬ φ → ψ) → χ) → (θ → χ)))
Theorem	luklem4 1426	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((¬ φ → φ) → φ) → ψ) → ψ)
Theorem	luklem5 1427	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (φ → (ψ → φ))
Theorem	luklem6 1428	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((φ → (φ → ψ)) → (φ → ψ))
Theorem	luklem7 1429	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((φ → (ψ → χ)) → (ψ → (φ → χ)))
Theorem	luklem8 1430	Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((φ → ψ) → ((χ → φ) → (χ → ψ)))
Theorem	ax1 1431	Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (φ → (ψ → φ))
Theorem	ax2 1432	Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((φ → (ψ → χ)) → ((φ → ψ) → (φ → χ)))
Theorem	ax3 1433	Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((¬ φ → ¬ ψ) → (ψ → φ))
1.3.3  Derive Nicod's axiom from the standard axioms Prove Nicod's axiom and implication and negation definitions.
Theorem	nic-dfim 1434	Define implication in terms of 'nand'. Analogous to ((φ ⊼ (ψ ⊼ ψ)) ↔ (φ → ψ)). 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 1435	Define negation in terms of 'nand'. Analogous to ((φ ⊼ φ) ↔ ¬ φ). 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 1436	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 1438. 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 1437	A direct proof of nic-mp 1436. (Contributed by NM, 30-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ φ    &   ⊢ (φ ⊼ (χ ⊼ ψ))    ⇒   ⊢ ψ
Theorem	nic-ax 1438	Nicod's axiom derived from the standard ones. See Intro. to Math. Phil. by B. Russell, p. 152. Like meredith 1404, the usual axioms can be derived from this and vice versa. Unlike meredith 1404, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g. { nic-ax 1438, nic-mp 1436 } is equivalent to { luk-1 1420, luk-2 1421, luk-3 1422, 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 1439	A direct proof of nic-ax 1438. (Contributed by NM, 11-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((φ ⊼ (χ ⊼ ψ)) ⊼ ((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))))
1.3.4  Derive the Lukasiewicz axioms from Nicod's axiom
Theorem	nic-imp 1440	Inference for nic-mp 1436 using nic-ax 1438 as major premise. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (φ ⊼ (χ ⊼ ψ))    ⇒   ⊢ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))
Theorem	nic-idlem1 1441	Lemma for nic-id 1443. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((θ ⊼ (τ ⊼ (τ ⊼ τ))) ⊼ (((φ ⊼ (χ ⊼ ψ)) ⊼ θ) ⊼ ((φ ⊼ (χ ⊼ ψ)) ⊼ θ)))
Theorem	nic-idlem2 1442	Lemma for nic-id 1443. Inference used by nic-id 1443. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (η ⊼ ((φ ⊼ (χ ⊼ ψ)) ⊼ θ))    ⇒   ⊢ ((θ ⊼ (τ ⊼ (τ ⊼ τ))) ⊼ η)
Theorem	nic-id 1443	Theorem id 19 expressed with ⊼. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (τ ⊼ (τ ⊼ τ))
Theorem	nic-swap 1444	⊼ is symmetric. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((θ ⊼ φ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))
Theorem	nic-isw1 1445	Inference version of nic-swap 1444. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (θ ⊼ φ)    ⇒   ⊢ (φ ⊼ θ)
Theorem	nic-isw2 1446	Inference for swapping nested terms. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (ψ ⊼ (θ ⊼ φ))    ⇒   ⊢ (ψ ⊼ (φ ⊼ θ))
Theorem	nic-iimp1 1447	Inference version of nic-imp 1440 using right-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (φ ⊼ (χ ⊼ ψ))    &   ⊢ (θ ⊼ χ)    ⇒   ⊢ (θ ⊼ φ)
Theorem	nic-iimp2 1448	Inference version of nic-imp 1440 using left-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((φ ⊼ ψ) ⊼ (χ ⊼ χ))    &   ⊢ (θ ⊼ φ)    ⇒   ⊢ (θ ⊼ (χ ⊼ χ))
Theorem	nic-idel 1449	Inference to remove the trailing term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (φ ⊼ (χ ⊼ ψ))    ⇒   ⊢ (φ ⊼ (χ ⊼ χ))
Theorem	nic-ich 1450	Chained inference. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (φ ⊼ (ψ ⊼ ψ))    &   ⊢ (ψ ⊼ (χ ⊼ χ))    ⇒   ⊢ (φ ⊼ (χ ⊼ χ))
Theorem	nic-idbl 1451	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 1452	For nic-* definitions, the biconditional connective is not used. Instead, definitions are made based on this form. nic-bi1 1453 and nic-bi2 1454 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 1453	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 1454	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 1455	Derive the standard modus ponens from nic-mp 1436. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ φ    &   ⊢ (φ → ψ)    ⇒   ⊢ ψ
Theorem	nic-luk1 1456	Proof of luk-1 1420 from nic-ax 1438 and nic-mp 1436 (and Definitions nic-dfim 1434 and nic-dfneg 1435). Note that the standard axioms ax-1 6, ax-2 7, and ax-3 8 are proved from the Lukasiewicz axioms by Theorems ax1 1431, ax2 1432, and ax3 1433. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((φ → ψ) → ((ψ → χ) → (φ → χ)))
Theorem	nic-luk2 1457	Proof of luk-2 1421 from nic-ax 1438 and nic-mp 1436. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((¬ φ → φ) → φ)
Theorem	nic-luk3 1458	Proof of luk-3 1422 from nic-ax 1438 and nic-mp 1436. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (φ → (¬ φ → ψ))
1.3.5  Derive Nicod's Axiom from Lukasiewicz's First Sheffer Stroke Axiom
Theorem	lukshef-ax1 1459	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 1436 for its constructions. Here, the axiom is proved as a substitution instance of nic-ax 1438. (Contributed by Anthony Hart, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((φ ⊼ (χ ⊼ ψ)) ⊼ ((θ ⊼ (θ ⊼ θ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))))
Theorem	lukshefth1 1460	Lemma for renicax 1462. (Contributed by NM, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ))) ⊼ (θ ⊼ (θ ⊼ θ))) ⊼ (φ ⊼ (ψ ⊼ χ)))
Theorem	lukshefth2 1461	Lemma for renicax 1462. (Contributed by NM, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((τ ⊼ θ) ⊼ ((θ ⊼ τ) ⊼ (θ ⊼ τ)))
Theorem	renicax 1462	A rederivation of nic-ax 1438 from lukshef-ax1 1459, proving that lukshef-ax1 1459 with nic-mp 1436 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.6  Derive the Lukasiewicz Axioms from the Tarski-Bernays-Wajsberg Axioms
Theorem	tbw-bijust 1463	Justification for tbw-negdf 1464. (Contributed by Anthony Hart, 15-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((φ ↔ ψ) ↔ (((φ → ψ) → ((ψ → φ) → ⊥ )) → ⊥ ))
Theorem	tbw-negdf 1464	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 1465	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 1466	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 1467	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 1468	The fourth of four axioms in the Tarski-Bernays-Wajsberg system. This axiom was added to the Tarski-Bernays axiom system ( see tb-ax1 , tb-ax2 , and tb-ax3 in set.mm) by Wajsberg for completeness. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ( ⊥ → φ)
Theorem	tbwsyl 1469	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 1470	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 1471	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 1472	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 1473	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 1474	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 1475	luk-1 1420 derived from the Tarski-Bernays-Wajsberg axioms. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((φ → ψ) → ((ψ → χ) → (φ → χ)))
Theorem	re1luk2 1476	luk-2 1421 derived from the Tarski-Bernays-Wajsberg axioms. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((¬ φ → φ) → φ)
Theorem	re1luk3 1477	luk-3 1422 derived from the Tarski-Bernays-Wajsberg axioms. This theorem, along with re1luk1 1475 and re1luk2 1476 proves that tbw-ax1 1465, tbw-ax2 1466, tbw-ax3 1467, and tbw-ax4 1468, 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.7  Derive the Tarski-Bernays-Wajsberg axioms from Meredith's First CO Axiom
Theorem	merco1 1478	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 1404 has 21 symbols, sans parentheses. See merco2 1501 for another axiom of equal length. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((((φ → ψ) → (χ → ⊥ )) → θ) → τ) → ((τ → φ) → (χ → φ)))
Theorem	merco1lem1 1479	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (φ → ( ⊥ → χ))
Theorem	retbwax4 1480	tbw-ax4 1468 rederived from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ( ⊥ → φ)
Theorem	retbwax2 1481	tbw-ax2 1466 rederived from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (φ → (ψ → φ))
Theorem	merco1lem2 1482	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((φ → ψ) → χ) → (((ψ → τ) → (φ → ⊥ )) → χ))
Theorem	merco1lem3 1483	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((φ → ψ) → (χ → ⊥ )) → (χ → φ))
Theorem	merco1lem4 1484	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((φ → ψ) → χ) → (ψ → χ))
Theorem	merco1lem5 1485	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((φ → ⊥ ) → χ) → τ) → (φ → τ))
Theorem	merco1lem6 1486	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((φ → (φ → ψ)) → (χ → (φ → ψ)))
Theorem	merco1lem7 1487	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (φ → (((ψ → χ) → ψ) → ψ))
Theorem	retbwax3 1488	tbw-ax3 1467 rederived from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((φ → ψ) → φ) → φ)
Theorem	merco1lem8 1489	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (φ → ((ψ → (ψ → χ)) → (ψ → χ)))
Theorem	merco1lem9 1490	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((φ → (φ → ψ)) → (φ → ψ))
Theorem	merco1lem10 1491	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((((φ → ψ) → χ) → (τ → χ)) → φ) → (θ → φ))
Theorem	merco1lem11 1492	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((φ → ψ) → (((χ → (φ → τ)) → ⊥ ) → ψ))
Theorem	merco1lem12 1493	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((φ → ψ) → (((χ → (φ → τ)) → φ) → ψ))
Theorem	merco1lem13 1494	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((φ → ψ) → (χ → ψ)) → τ) → (φ → τ))
Theorem	merco1lem14 1495	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((((φ → ψ) → ψ) → χ) → (φ → χ))
Theorem	merco1lem15 1496	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((φ → ψ) → (φ → (χ → ψ)))
Theorem	merco1lem16 1497	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((φ → (ψ → χ)) → τ) → ((φ → χ) → τ))
Theorem	merco1lem17 1498	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (((((φ → ψ) → φ) → χ) → τ) → ((φ → χ) → τ))
Theorem	merco1lem18 1499	Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ)))
Theorem	retbwax1 1500	tbw-ax1 1465 rederived from merco1 1478. This theorem, along with retbwax2 1481, retbwax3 1488, and retbwax4 1480, shows that merco1 1478 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.)
⊢ ((φ → ψ) → ((ψ → χ) → (φ → χ)))