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 ( ( 𝜑𝜓 ) → ( ( 𝜓𝜒 ) → ( 𝜑𝜒 ) ) )