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 
|- ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) )

Proof

Step Hyp Ref Expression
1 nic-dfim 
 |-  ( ( ( ph -/\ ( ps -/\ ps ) ) -/\ ( ph -> ps ) ) -/\ ( ( ( ph -/\ ( ps -/\ ps ) ) -/\ ( ph -/\ ( ps -/\ ps ) ) ) -/\ ( ( ph -> ps ) -/\ ( ph -> ps ) ) ) )
2 1 nic-bi2 
 |-  ( ( ph -> ps ) -/\ ( ( ph -/\ ( ps -/\ ps ) ) -/\ ( ph -/\ ( ps -/\ ps ) ) ) )
3 nic-ax 
 |-  ( ( ph -/\ ( ps -/\ ps ) ) -/\ ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( ( ch -/\ ch ) -/\ ps ) -/\ ( ( ph -/\ ( ch -/\ ch ) ) -/\ ( ph -/\ ( ch -/\ ch ) ) ) ) ) )
4 3 nic-isw2 
 |-  ( ( ph -/\ ( ps -/\ ps ) ) -/\ ( ( ( ( ch -/\ ch ) -/\ ps ) -/\ ( ( ph -/\ ( ch -/\ ch ) ) -/\ ( ph -/\ ( ch -/\ ch ) ) ) ) -/\ ( ta -/\ ( ta -/\ ta ) ) ) )
5 4 nic-idel 
 |-  ( ( ph -/\ ( ps -/\ ps ) ) -/\ ( ( ( ( ch -/\ ch ) -/\ ps ) -/\ ( ( ph -/\ ( ch -/\ ch ) ) -/\ ( ph -/\ ( ch -/\ ch ) ) ) ) -/\ ( ( ( ch -/\ ch ) -/\ ps ) -/\ ( ( ph -/\ ( ch -/\ ch ) ) -/\ ( ph -/\ ( ch -/\ ch ) ) ) ) ) )
6 nic-dfim 
 |-  ( ( ( ph -/\ ( ch -/\ ch ) ) -/\ ( ph -> ch ) ) -/\ ( ( ( ph -/\ ( ch -/\ ch ) ) -/\ ( ph -/\ ( ch -/\ ch ) ) ) -/\ ( ( ph -> ch ) -/\ ( ph -> ch ) ) ) )
7 6 nic-bi1 
 |-  ( ( ph -/\ ( ch -/\ ch ) ) -/\ ( ( ph -> ch ) -/\ ( ph -> ch ) ) )
8 7 nic-idbl 
 |-  ( ( ( ph -> ch ) -/\ ( ph -> ch ) ) -/\ ( ( ( ph -/\ ( ch -/\ ch ) ) -/\ ( ph -/\ ( ch -/\ ch ) ) ) -/\ ( ( ph -/\ ( ch -/\ ch ) ) -/\ ( ph -/\ ( ch -/\ ch ) ) ) ) )
9 8 nic-imp 
 |-  ( ( ( ( ch -/\ ch ) -/\ ps ) -/\ ( ( ph -/\ ( ch -/\ ch ) ) -/\ ( ph -/\ ( ch -/\ ch ) ) ) ) -/\ ( ( ( ( ph -> ch ) -/\ ( ph -> ch ) ) -/\ ( ( ch -/\ ch ) -/\ ps ) ) -/\ ( ( ( ph -> ch ) -/\ ( ph -> ch ) ) -/\ ( ( ch -/\ ch ) -/\ ps ) ) ) )
10 nic-dfim 
 |-  ( ( ( ps -/\ ( ch -/\ ch ) ) -/\ ( ps -> ch ) ) -/\ ( ( ( ps -/\ ( ch -/\ ch ) ) -/\ ( ps -/\ ( ch -/\ ch ) ) ) -/\ ( ( ps -> ch ) -/\ ( ps -> ch ) ) ) )
11 10 nic-bi2 
 |-  ( ( ps -> ch ) -/\ ( ( ps -/\ ( ch -/\ ch ) ) -/\ ( ps -/\ ( ch -/\ ch ) ) ) )
12 nic-swap 
 |-  ( ( ps -/\ ( ch -/\ ch ) ) -/\ ( ( ( ch -/\ ch ) -/\ ps ) -/\ ( ( ch -/\ ch ) -/\ ps ) ) )
13 11 12 nic-ich 
 |-  ( ( ps -> ch ) -/\ ( ( ( ch -/\ ch ) -/\ ps ) -/\ ( ( ch -/\ ch ) -/\ ps ) ) )
14 13 nic-imp 
 |-  ( ( ( ( ph -> ch ) -/\ ( ph -> ch ) ) -/\ ( ( ch -/\ ch ) -/\ ps ) ) -/\ ( ( ( ps -> ch ) -/\ ( ( ph -> ch ) -/\ ( ph -> ch ) ) ) -/\ ( ( ps -> ch ) -/\ ( ( ph -> ch ) -/\ ( ph -> ch ) ) ) ) )
15 9 14 nic-ich 
 |-  ( ( ( ( ch -/\ ch ) -/\ ps ) -/\ ( ( ph -/\ ( ch -/\ ch ) ) -/\ ( ph -/\ ( ch -/\ ch ) ) ) ) -/\ ( ( ( ps -> ch ) -/\ ( ( ph -> ch ) -/\ ( ph -> ch ) ) ) -/\ ( ( ps -> ch ) -/\ ( ( ph -> ch ) -/\ ( ph -> ch ) ) ) ) )
16 5 15 nic-ich 
 |-  ( ( ph -/\ ( ps -/\ ps ) ) -/\ ( ( ( ps -> ch ) -/\ ( ( ph -> ch ) -/\ ( ph -> ch ) ) ) -/\ ( ( ps -> ch ) -/\ ( ( ph -> ch ) -/\ ( ph -> ch ) ) ) ) )
17 nic-dfim 
 |-  ( ( ( ( ps -> ch ) -/\ ( ( ph -> ch ) -/\ ( ph -> ch ) ) ) -/\ ( ( ps -> ch ) -> ( ph -> ch ) ) ) -/\ ( ( ( ( ps -> ch ) -/\ ( ( ph -> ch ) -/\ ( ph -> ch ) ) ) -/\ ( ( ps -> ch ) -/\ ( ( ph -> ch ) -/\ ( ph -> ch ) ) ) ) -/\ ( ( ( ps -> ch ) -> ( ph -> ch ) ) -/\ ( ( ps -> ch ) -> ( ph -> ch ) ) ) ) )
18 17 nic-bi1 
 |-  ( ( ( ps -> ch ) -/\ ( ( ph -> ch ) -/\ ( ph -> ch ) ) ) -/\ ( ( ( ps -> ch ) -> ( ph -> ch ) ) -/\ ( ( ps -> ch ) -> ( ph -> ch ) ) ) )
19 16 18 nic-ich 
 |-  ( ( ph -/\ ( ps -/\ ps ) ) -/\ ( ( ( ps -> ch ) -> ( ph -> ch ) ) -/\ ( ( ps -> ch ) -> ( ph -> ch ) ) ) )
20 2 19 nic-ich 
 |-  ( ( ph -> ps ) -/\ ( ( ( ps -> ch ) -> ( ph -> ch ) ) -/\ ( ( ps -> ch ) -> ( ph -> ch ) ) ) )
21 nic-dfim 
 |-  ( ( ( ( ph -> ps ) -/\ ( ( ( ps -> ch ) -> ( ph -> ch ) ) -/\ ( ( ps -> ch ) -> ( ph -> ch ) ) ) ) -/\ ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) ) -/\ ( ( ( ( ph -> ps ) -/\ ( ( ( ps -> ch ) -> ( ph -> ch ) ) -/\ ( ( ps -> ch ) -> ( ph -> ch ) ) ) ) -/\ ( ( ph -> ps ) -/\ ( ( ( ps -> ch ) -> ( ph -> ch ) ) -/\ ( ( ps -> ch ) -> ( ph -> ch ) ) ) ) ) -/\ ( ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) -/\ ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) ) ) )
22 21 nic-bi1 
 |-  ( ( ( ph -> ps ) -/\ ( ( ( ps -> ch ) -> ( ph -> ch ) ) -/\ ( ( ps -> ch ) -> ( ph -> ch ) ) ) ) -/\ ( ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) -/\ ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) ) ) )
23 20 22 nic-mp 
 |-  ( ( ph -> ps ) -> ( ( ps -> ch ) -> ( ph -> ch ) ) )