Theorem nic-luk1 1456

Description: Proof of luk-1 1420 from nic-ax 1438 and nic-mp 1436 (and definitions nic-dfim 1434 and nic-dfneg 1435). Note that the standard axioms ax-1 6, ax-2 7, and ax-3 8 are proved from the Lukasiewicz axioms by theorems ax1 1431, ax2 1432, and ax3 1433. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
nic-luk1	⊢ ((φ → ψ) → ((ψ → χ) → (φ → χ)))

Proof of Theorem nic-luk1

Step	Hyp	Ref	Expression
1		nic-dfim 1434	. . . 4 ⊢ (((φ ⊼ (ψ ⊼ ψ)) ⊼ (φ → ψ)) ⊼ (((φ ⊼ (ψ ⊼ ψ)) ⊼ (φ ⊼ (ψ ⊼ ψ))) ⊼ ((φ → ψ) ⊼ (φ → ψ))))
2	1	nic-bi2 1454	. . 3 ⊢ ((φ → ψ) ⊼ ((φ ⊼ (ψ ⊼ ψ)) ⊼ (φ ⊼ (ψ ⊼ ψ))))
3		nic-ax 1438	. . . . . . 7 ⊢ ((φ ⊼ (ψ ⊼ ψ)) ⊼ ((τ ⊼ (τ ⊼ τ)) ⊼ (((χ ⊼ χ) ⊼ ψ) ⊼ ((φ ⊼ (χ ⊼ χ)) ⊼ (φ ⊼ (χ ⊼ χ))))))
4	3	nic-isw2 1446	. . . . . 6 ⊢ ((φ ⊼ (ψ ⊼ ψ)) ⊼ ((((χ ⊼ χ) ⊼ ψ) ⊼ ((φ ⊼ (χ ⊼ χ)) ⊼ (φ ⊼ (χ ⊼ χ)))) ⊼ (τ ⊼ (τ ⊼ τ))))
5	4	nic-idel 1449	. . . . 5 ⊢ ((φ ⊼ (ψ ⊼ ψ)) ⊼ ((((χ ⊼ χ) ⊼ ψ) ⊼ ((φ ⊼ (χ ⊼ χ)) ⊼ (φ ⊼ (χ ⊼ χ)))) ⊼ (((χ ⊼ χ) ⊼ ψ) ⊼ ((φ ⊼ (χ ⊼ χ)) ⊼ (φ ⊼ (χ ⊼ χ))))))
6		nic-dfim 1434	. . . . . . . . 9 ⊢ (((φ ⊼ (χ ⊼ χ)) ⊼ (φ → χ)) ⊼ (((φ ⊼ (χ ⊼ χ)) ⊼ (φ ⊼ (χ ⊼ χ))) ⊼ ((φ → χ) ⊼ (φ → χ))))
7	6	nic-bi1 1453	. . . . . . . 8 ⊢ ((φ ⊼ (χ ⊼ χ)) ⊼ ((φ → χ) ⊼ (φ → χ)))
8	7	nic-idbl 1451	. . . . . . 7 ⊢ (((φ → χ) ⊼ (φ → χ)) ⊼ (((φ ⊼ (χ ⊼ χ)) ⊼ (φ ⊼ (χ ⊼ χ))) ⊼ ((φ ⊼ (χ ⊼ χ)) ⊼ (φ ⊼ (χ ⊼ χ)))))
9	8	nic-imp 1440	. . . . . 6 ⊢ ((((χ ⊼ χ) ⊼ ψ) ⊼ ((φ ⊼ (χ ⊼ χ)) ⊼ (φ ⊼ (χ ⊼ χ)))) ⊼ ((((φ → χ) ⊼ (φ → χ)) ⊼ ((χ ⊼ χ) ⊼ ψ)) ⊼ (((φ → χ) ⊼ (φ → χ)) ⊼ ((χ ⊼ χ) ⊼ ψ))))
10		nic-dfim 1434	. . . . . . . . 9 ⊢ (((ψ ⊼ (χ ⊼ χ)) ⊼ (ψ → χ)) ⊼ (((ψ ⊼ (χ ⊼ χ)) ⊼ (ψ ⊼ (χ ⊼ χ))) ⊼ ((ψ → χ) ⊼ (ψ → χ))))
11	10	nic-bi2 1454	. . . . . . . 8 ⊢ ((ψ → χ) ⊼ ((ψ ⊼ (χ ⊼ χ)) ⊼ (ψ ⊼ (χ ⊼ χ))))
12		nic-swap 1444	. . . . . . . 8 ⊢ ((ψ ⊼ (χ ⊼ χ)) ⊼ (((χ ⊼ χ) ⊼ ψ) ⊼ ((χ ⊼ χ) ⊼ ψ)))
13	11, 12	nic-ich 1450	. . . . . . 7 ⊢ ((ψ → χ) ⊼ (((χ ⊼ χ) ⊼ ψ) ⊼ ((χ ⊼ χ) ⊼ ψ)))
14	13	nic-imp 1440	. . . . . 6 ⊢ ((((φ → χ) ⊼ (φ → χ)) ⊼ ((χ ⊼ χ) ⊼ ψ)) ⊼ (((ψ → χ) ⊼ ((φ → χ) ⊼ (φ → χ))) ⊼ ((ψ → χ) ⊼ ((φ → χ) ⊼ (φ → χ)))))
15	9, 14	nic-ich 1450	. . . . 5 ⊢ ((((χ ⊼ χ) ⊼ ψ) ⊼ ((φ ⊼ (χ ⊼ χ)) ⊼ (φ ⊼ (χ ⊼ χ)))) ⊼ (((ψ → χ) ⊼ ((φ → χ) ⊼ (φ → χ))) ⊼ ((ψ → χ) ⊼ ((φ → χ) ⊼ (φ → χ)))))
16	5, 15	nic-ich 1450	. . . 4 ⊢ ((φ ⊼ (ψ ⊼ ψ)) ⊼ (((ψ → χ) ⊼ ((φ → χ) ⊼ (φ → χ))) ⊼ ((ψ → χ) ⊼ ((φ → χ) ⊼ (φ → χ)))))
17		nic-dfim 1434	. . . . 5 ⊢ ((((ψ → χ) ⊼ ((φ → χ) ⊼ (φ → χ))) ⊼ ((ψ → χ) → (φ → χ))) ⊼ ((((ψ → χ) ⊼ ((φ → χ) ⊼ (φ → χ))) ⊼ ((ψ → χ) ⊼ ((φ → χ) ⊼ (φ → χ)))) ⊼ (((ψ → χ) → (φ → χ)) ⊼ ((ψ → χ) → (φ → χ)))))
18	17	nic-bi1 1453	. . . 4 ⊢ (((ψ → χ) ⊼ ((φ → χ) ⊼ (φ → χ))) ⊼ (((ψ → χ) → (φ → χ)) ⊼ ((ψ → χ) → (φ → χ))))
19	16, 18	nic-ich 1450	. . 3 ⊢ ((φ ⊼ (ψ ⊼ ψ)) ⊼ (((ψ → χ) → (φ → χ)) ⊼ ((ψ → χ) → (φ → χ))))
20	2, 19	nic-ich 1450	. 2 ⊢ ((φ → ψ) ⊼ (((ψ → χ) → (φ → χ)) ⊼ ((ψ → χ) → (φ → χ))))
21		nic-dfim 1434	. . 3 ⊢ ((((φ → ψ) ⊼ (((ψ → χ) → (φ → χ)) ⊼ ((ψ → χ) → (φ → χ)))) ⊼ ((φ → ψ) → ((ψ → χ) → (φ → χ)))) ⊼ ((((φ → ψ) ⊼ (((ψ → χ) → (φ → χ)) ⊼ ((ψ → χ) → (φ → χ)))) ⊼ ((φ → ψ) ⊼ (((ψ → χ) → (φ → χ)) ⊼ ((ψ → χ) → (φ → χ))))) ⊼ (((φ → ψ) → ((ψ → χ) → (φ → χ))) ⊼ ((φ → ψ) → ((ψ → χ) → (φ → χ))))))
22	21	nic-bi1 1453	. 2 ⊢ (((φ → ψ) ⊼ (((ψ → χ) → (φ → χ)) ⊼ ((ψ → χ) → (φ → χ)))) ⊼ (((φ → ψ) → ((ψ → χ) → (φ → χ))) ⊼ ((φ → ψ) → ((ψ → χ) → (φ → χ)))))
23	20, 22	nic-mp 1436	1 ⊢ ((φ → ψ) → ((ψ → χ) → (φ → χ)))

Syntax hints:   → wi 4   ⊼ 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-or 359  df-an 360  df-nan 1288

This theorem is referenced by: (None)