MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nic-luk1 Structured version   Visualization version   GIF version

Theorem nic-luk1 1765
Description: Proof of luk-1 1729 from nic-ax 1747 and nic-mp 1745 (and definitions nic-dfim 1743 and nic-dfneg 1744). Note that the standard axioms ax-1 6, ax-2 7, and ax-3 8 are proved from the Lukasiewicz axioms by theorems ax1 1740, ax2 1741, and ax3 1742. (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
StepHypRef Expression
1 nic-dfim 1743 . . . 4 (((𝜑 ⊼ (𝜓𝜓)) ⊼ (𝜑𝜓)) ⊼ (((𝜑 ⊼ (𝜓𝜓)) ⊼ (𝜑 ⊼ (𝜓𝜓))) ⊼ ((𝜑𝜓) ⊼ (𝜑𝜓))))
21nic-bi2 1763 . . 3 ((𝜑𝜓) ⊼ ((𝜑 ⊼ (𝜓𝜓)) ⊼ (𝜑 ⊼ (𝜓𝜓))))
3 nic-ax 1747 . . . . . . 7 ((𝜑 ⊼ (𝜓𝜓)) ⊼ ((𝜏 ⊼ (𝜏𝜏)) ⊼ (((𝜒𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒𝜒)) ⊼ (𝜑 ⊼ (𝜒𝜒))))))
43nic-isw2 1755 . . . . . 6 ((𝜑 ⊼ (𝜓𝜓)) ⊼ ((((𝜒𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒𝜒)) ⊼ (𝜑 ⊼ (𝜒𝜒)))) ⊼ (𝜏 ⊼ (𝜏𝜏))))
54nic-idel 1758 . . . . 5 ((𝜑 ⊼ (𝜓𝜓)) ⊼ ((((𝜒𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒𝜒)) ⊼ (𝜑 ⊼ (𝜒𝜒)))) ⊼ (((𝜒𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒𝜒)) ⊼ (𝜑 ⊼ (𝜒𝜒))))))
6 nic-dfim 1743 . . . . . . . . 9 (((𝜑 ⊼ (𝜒𝜒)) ⊼ (𝜑𝜒)) ⊼ (((𝜑 ⊼ (𝜒𝜒)) ⊼ (𝜑 ⊼ (𝜒𝜒))) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒))))
76nic-bi1 1762 . . . . . . . 8 ((𝜑 ⊼ (𝜒𝜒)) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒)))
87nic-idbl 1760 . . . . . . 7 (((𝜑𝜒) ⊼ (𝜑𝜒)) ⊼ (((𝜑 ⊼ (𝜒𝜒)) ⊼ (𝜑 ⊼ (𝜒𝜒))) ⊼ ((𝜑 ⊼ (𝜒𝜒)) ⊼ (𝜑 ⊼ (𝜒𝜒)))))
98nic-imp 1749 . . . . . 6 ((((𝜒𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒𝜒)) ⊼ (𝜑 ⊼ (𝜒𝜒)))) ⊼ ((((𝜑𝜒) ⊼ (𝜑𝜒)) ⊼ ((𝜒𝜒) ⊼ 𝜓)) ⊼ (((𝜑𝜒) ⊼ (𝜑𝜒)) ⊼ ((𝜒𝜒) ⊼ 𝜓))))
10 nic-dfim 1743 . . . . . . . . 9 (((𝜓 ⊼ (𝜒𝜒)) ⊼ (𝜓𝜒)) ⊼ (((𝜓 ⊼ (𝜒𝜒)) ⊼ (𝜓 ⊼ (𝜒𝜒))) ⊼ ((𝜓𝜒) ⊼ (𝜓𝜒))))
1110nic-bi2 1763 . . . . . . . 8 ((𝜓𝜒) ⊼ ((𝜓 ⊼ (𝜒𝜒)) ⊼ (𝜓 ⊼ (𝜒𝜒))))
12 nic-swap 1753 . . . . . . . 8 ((𝜓 ⊼ (𝜒𝜒)) ⊼ (((𝜒𝜒) ⊼ 𝜓) ⊼ ((𝜒𝜒) ⊼ 𝜓)))
1311, 12nic-ich 1759 . . . . . . 7 ((𝜓𝜒) ⊼ (((𝜒𝜒) ⊼ 𝜓) ⊼ ((𝜒𝜒) ⊼ 𝜓)))
1413nic-imp 1749 . . . . . 6 ((((𝜑𝜒) ⊼ (𝜑𝜒)) ⊼ ((𝜒𝜒) ⊼ 𝜓)) ⊼ (((𝜓𝜒) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒))) ⊼ ((𝜓𝜒) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒)))))
159, 14nic-ich 1759 . . . . 5 ((((𝜒𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒𝜒)) ⊼ (𝜑 ⊼ (𝜒𝜒)))) ⊼ (((𝜓𝜒) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒))) ⊼ ((𝜓𝜒) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒)))))
165, 15nic-ich 1759 . . . 4 ((𝜑 ⊼ (𝜓𝜓)) ⊼ (((𝜓𝜒) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒))) ⊼ ((𝜓𝜒) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒)))))
17 nic-dfim 1743 . . . . 5 ((((𝜓𝜒) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒))) ⊼ ((𝜓𝜒) → (𝜑𝜒))) ⊼ ((((𝜓𝜒) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒))) ⊼ ((𝜓𝜒) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒)))) ⊼ (((𝜓𝜒) → (𝜑𝜒)) ⊼ ((𝜓𝜒) → (𝜑𝜒)))))
1817nic-bi1 1762 . . . 4 (((𝜓𝜒) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒))) ⊼ (((𝜓𝜒) → (𝜑𝜒)) ⊼ ((𝜓𝜒) → (𝜑𝜒))))
1916, 18nic-ich 1759 . . 3 ((𝜑 ⊼ (𝜓𝜓)) ⊼ (((𝜓𝜒) → (𝜑𝜒)) ⊼ ((𝜓𝜒) → (𝜑𝜒))))
202, 19nic-ich 1759 . 2 ((𝜑𝜓) ⊼ (((𝜓𝜒) → (𝜑𝜒)) ⊼ ((𝜓𝜒) → (𝜑𝜒))))
21 nic-dfim 1743 . . 3 ((((𝜑𝜓) ⊼ (((𝜓𝜒) → (𝜑𝜒)) ⊼ ((𝜓𝜒) → (𝜑𝜒)))) ⊼ ((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒)))) ⊼ ((((𝜑𝜓) ⊼ (((𝜓𝜒) → (𝜑𝜒)) ⊼ ((𝜓𝜒) → (𝜑𝜒)))) ⊼ ((𝜑𝜓) ⊼ (((𝜓𝜒) → (𝜑𝜒)) ⊼ ((𝜓𝜒) → (𝜑𝜒))))) ⊼ (((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒))) ⊼ ((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒))))))
2221nic-bi1 1762 . 2 (((𝜑𝜓) ⊼ (((𝜓𝜒) → (𝜑𝜒)) ⊼ ((𝜓𝜒) → (𝜑𝜒)))) ⊼ (((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒))) ⊼ ((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒)))))
2320, 22nic-mp 1745 1 ((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnan 1596
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 197  df-or 384  df-an 385  df-nan 1597
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator