Metamath Proof Explorer


Theorem nic-luk1

Description: Proof of luk-1 from nic-ax and nic-mp (and Definitions nic-dfim and nic-dfneg ). Note that the standard axioms ax-1 , ax-2 , and ax-3 are proved from the Lukasiewicz axioms by Theorems ax1 , ax2 , and ax3 . (Contributed by Jeff Hoffman, 18-Nov-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion nic-luk1 φ ψ ψ χ φ χ

Proof

Step Hyp Ref Expression
1 nic-dfim φ ψ ψ φ ψ φ ψ ψ φ ψ ψ φ ψ φ ψ
2 1 nic-bi2 φ ψ φ ψ ψ φ ψ ψ
3 nic-ax φ ψ ψ τ τ τ χ χ ψ φ χ χ φ χ χ
4 3 nic-isw2 φ ψ ψ χ χ ψ φ χ χ φ χ χ τ τ τ
5 4 nic-idel φ ψ ψ χ χ ψ φ χ χ φ χ χ χ χ ψ φ χ χ φ χ χ
6 nic-dfim φ χ χ φ χ φ χ χ φ χ χ φ χ φ χ
7 6 nic-bi1 φ χ χ φ χ φ χ
8 7 nic-idbl φ χ φ χ φ χ χ φ χ χ φ χ χ φ χ χ
9 8 nic-imp χ χ ψ φ χ χ φ χ χ φ χ φ χ χ χ ψ φ χ φ χ χ χ ψ
10 nic-dfim ψ χ χ ψ χ ψ χ χ ψ χ χ ψ χ ψ χ
11 10 nic-bi2 ψ χ ψ χ χ ψ χ χ
12 nic-swap ψ χ χ χ χ ψ χ χ ψ
13 11 12 nic-ich ψ χ χ χ ψ χ χ ψ
14 13 nic-imp φ χ φ χ χ χ ψ ψ χ φ χ φ χ ψ χ φ χ φ χ
15 9 14 nic-ich χ χ ψ φ χ χ φ χ χ ψ χ φ χ φ χ ψ χ φ χ φ χ
16 5 15 nic-ich φ ψ ψ ψ χ φ χ φ χ ψ χ φ χ φ χ
17 nic-dfim ψ χ φ χ φ χ ψ χ φ χ ψ χ φ χ φ χ ψ χ φ χ φ χ ψ χ φ χ ψ χ φ χ
18 17 nic-bi1 ψ χ φ χ φ χ ψ χ φ χ ψ χ φ χ
19 16 18 nic-ich φ ψ ψ ψ χ φ χ ψ χ φ χ
20 2 19 nic-ich φ ψ ψ χ φ χ ψ χ φ χ
21 nic-dfim φ ψ ψ χ φ χ ψ χ φ χ φ ψ ψ χ φ χ φ ψ ψ χ φ χ ψ χ φ χ φ ψ ψ χ φ χ ψ χ φ χ φ ψ ψ χ φ χ φ ψ ψ χ φ χ
22 21 nic-bi1 φ ψ ψ χ φ χ ψ χ φ χ φ ψ ψ χ φ χ φ ψ ψ χ φ χ
23 20 22 nic-mp φ ψ ψ χ φ χ