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

Theorem lukshef-ax1 1450
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 1427 for its constructions.

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

Assertion
Ref Expression
lukshef-ax1  |-  ( (
ph  -/\  ( ch  -/\  ps ) )  -/\  (
( th  -/\  ( th  -/\  th ) ) 
-/\  ( ( th 
-/\  ch )  -/\  (
( ph  -/\  th )  -/\  ( ph  -/\  th )
) ) ) )

Proof of Theorem lukshef-ax1
StepHypRef Expression
1 nic-ax 1429 1  |-  ( (
ph  -/\  ( ch  -/\  ps ) )  -/\  (
( th  -/\  ( th  -/\  th ) ) 
-/\  ( ( th 
-/\  ch )  -/\  (
( ph  -/\  th )  -/\  ( ph  -/\  th )
) ) ) )
Colors of variables: wff set class
Syntax hints:    -/\ wnan 1289
This theorem is referenced by:  lukshefth1  1451  lukshefth2  1452  renicax  1453
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362  df-nan 1290
  Copyright terms: Public domain W3C validator