lukshef-ax1 - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > lukshef-ax1		Unicode version

Theorem lukshef-ax1 1459

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 1436 for its constructions.

Here, the axiom is proved as a substitution instance of nic-ax 1438. (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 1438	1 $-/\$ $-/\$ $-/\$ $-/\$ $-/\$ $-/\$ $-/\$ $-/\$ $-/\$ $-/\$ $-/\$

Colors of variables: wff setvar class

Syntax hints: $-/\$ wnan 1287

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 177 df-an 360 df-nan 1288

This theorem is referenced by: lukshefth1 1460 lukshefth2 1461 renicax 1462

W3C validator