Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > lukshef-ax1 | Structured version Visualization version GIF version |
Description: 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 1587 for its constructions. Here, the axiom is proved as a substitution instance of nic-ax 1589. (Contributed by Anthony Hart, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
lukshef-ax1 | ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜃 ⊼ (𝜃 ⊼ 𝜃)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nic-ax 1589 | 1 ⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜃 ⊼ (𝜃 ⊼ 𝜃)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) |
Colors of variables: wff setvar class |
Syntax hints: ⊼ wnan 1439 |
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 196 df-an 385 df-nan 1440 |
This theorem is referenced by: lukshefth1 1611 lukshefth2 1612 renicax 1613 |
Copyright terms: Public domain | W3C validator |