Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > lukshefax1  Unicode 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 nicmp 1504 for its constructions. Here, the axiom is proved as a substitution instance of nicax 1506. (Contributed by Anthony Hart, 31Jul2011.) (Proof modification is discouraged.) (New usage is discouraged.) 
Ref  Expression 

lukshefax1 
Step  Hyp  Ref  Expression 

1  nicax 1506  1 
Colors of variables: wff setvar class 
Syntax hints: /\ wnan 1343 
This theorem is referenced by: lukshefth1 1528 lukshefth2 1529 renicax 1530 
This theorem was proved from axioms: axmp 5 ax1 6 ax2 7 ax3 8 
This theorem depends on definitions: dfbi 185 dfan 371 dfnan 1344 
Copyright terms: Public domain  W3C validator 