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 ⊢ φ → ψ → ψ → χ → φ → χ