Theorem lukshef-ax1 1722

Description: 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 1699 for its constructions.

Here, the axiom is proved as a substitution instance of nic-ax 1701. (Contributed by Anthony Hart, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
lukshef-ax1	⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜃 ⊼ (𝜃 ⊼ 𝜃)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))

Proof of Theorem lukshef-ax1

Step	Hyp	Ref	Expression
1		nic-ax 1701	1 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜃 ⊼ (𝜃 ⊼ 𝜃)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))

Syntax hints:   ⊼ wnan 1519

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401  df-nan 1520

This theorem is referenced by:  lukshefth1  1723  lukshefth2  1724  renicax  1725