 Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  lukshef-ax1 Structured version   Visualization version   GIF version

Theorem lukshef-ax1 1795
 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 1772 for its constructions. Here, the axiom is proved as a substitution instance of nic-ax 1774. (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
StepHypRef Expression
1 nic-ax 1774 1 ((𝜑 ⊼ (𝜒𝜓)) ⊼ ((𝜃 ⊼ (𝜃𝜃)) ⊼ ((𝜃𝜒) ⊼ ((𝜑𝜃) ⊼ (𝜑𝜃)))))
 Colors of variables: wff setvar class Syntax hints:   ⊼ wnan 1614 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 199  df-an 387  df-nan 1615 This theorem is referenced by:  lukshefth1  1796  lukshefth2  1797  renicax  1798
 Copyright terms: Public domain W3C validator