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 1607
Description: Proof of luk-1 1571 from nic-ax 1589 and nic-mp 1587 (and definitions nic-dfim 1585 and nic-dfneg 1586). Note that the standard axioms ax-1 6, ax-2 7, and ax-3 8 are proved from the Lukasiewicz axioms by theorems ax1 1582, ax2 1583, and ax3 1584. (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 1585 . . . 4 (((𝜑 ⊼ (𝜓𝜓)) ⊼ (𝜑𝜓)) ⊼ (((𝜑 ⊼ (𝜓𝜓)) ⊼ (𝜑 ⊼ (𝜓𝜓))) ⊼ ((𝜑𝜓) ⊼ (𝜑𝜓))))
21nic-bi2 1605 . . 3 ((𝜑𝜓) ⊼ ((𝜑 ⊼ (𝜓𝜓)) ⊼ (𝜑 ⊼ (𝜓𝜓))))
3 nic-ax 1589 . . . . . . 7 ((𝜑 ⊼ (𝜓𝜓)) ⊼ ((𝜏 ⊼ (𝜏𝜏)) ⊼ (((𝜒𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒𝜒)) ⊼ (𝜑 ⊼ (𝜒𝜒))))))
43nic-isw2 1597 . . . . . 6 ((𝜑 ⊼ (𝜓𝜓)) ⊼ ((((𝜒𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒𝜒)) ⊼ (𝜑 ⊼ (𝜒𝜒)))) ⊼ (𝜏 ⊼ (𝜏𝜏))))
54nic-idel 1600 . . . . 5 ((𝜑 ⊼ (𝜓𝜓)) ⊼ ((((𝜒𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒𝜒)) ⊼ (𝜑 ⊼ (𝜒𝜒)))) ⊼ (((𝜒𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒𝜒)) ⊼ (𝜑 ⊼ (𝜒𝜒))))))
6 nic-dfim 1585 . . . . . . . . 9 (((𝜑 ⊼ (𝜒𝜒)) ⊼ (𝜑𝜒)) ⊼ (((𝜑 ⊼ (𝜒𝜒)) ⊼ (𝜑 ⊼ (𝜒𝜒))) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒))))
76nic-bi1 1604 . . . . . . . 8 ((𝜑 ⊼ (𝜒𝜒)) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒)))
87nic-idbl 1602 . . . . . . 7 (((𝜑𝜒) ⊼ (𝜑𝜒)) ⊼ (((𝜑 ⊼ (𝜒𝜒)) ⊼ (𝜑 ⊼ (𝜒𝜒))) ⊼ ((𝜑 ⊼ (𝜒𝜒)) ⊼ (𝜑 ⊼ (𝜒𝜒)))))
98nic-imp 1591 . . . . . 6 ((((𝜒𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒𝜒)) ⊼ (𝜑 ⊼ (𝜒𝜒)))) ⊼ ((((𝜑𝜒) ⊼ (𝜑𝜒)) ⊼ ((𝜒𝜒) ⊼ 𝜓)) ⊼ (((𝜑𝜒) ⊼ (𝜑𝜒)) ⊼ ((𝜒𝜒) ⊼ 𝜓))))
10 nic-dfim 1585 . . . . . . . . 9 (((𝜓 ⊼ (𝜒𝜒)) ⊼ (𝜓𝜒)) ⊼ (((𝜓 ⊼ (𝜒𝜒)) ⊼ (𝜓 ⊼ (𝜒𝜒))) ⊼ ((𝜓𝜒) ⊼ (𝜓𝜒))))
1110nic-bi2 1605 . . . . . . . 8 ((𝜓𝜒) ⊼ ((𝜓 ⊼ (𝜒𝜒)) ⊼ (𝜓 ⊼ (𝜒𝜒))))
12 nic-swap 1595 . . . . . . . 8 ((𝜓 ⊼ (𝜒𝜒)) ⊼ (((𝜒𝜒) ⊼ 𝜓) ⊼ ((𝜒𝜒) ⊼ 𝜓)))
1311, 12nic-ich 1601 . . . . . . 7 ((𝜓𝜒) ⊼ (((𝜒𝜒) ⊼ 𝜓) ⊼ ((𝜒𝜒) ⊼ 𝜓)))
1413nic-imp 1591 . . . . . 6 ((((𝜑𝜒) ⊼ (𝜑𝜒)) ⊼ ((𝜒𝜒) ⊼ 𝜓)) ⊼ (((𝜓𝜒) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒))) ⊼ ((𝜓𝜒) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒)))))
159, 14nic-ich 1601 . . . . 5 ((((𝜒𝜒) ⊼ 𝜓) ⊼ ((𝜑 ⊼ (𝜒𝜒)) ⊼ (𝜑 ⊼ (𝜒𝜒)))) ⊼ (((𝜓𝜒) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒))) ⊼ ((𝜓𝜒) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒)))))
165, 15nic-ich 1601 . . . 4 ((𝜑 ⊼ (𝜓𝜓)) ⊼ (((𝜓𝜒) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒))) ⊼ ((𝜓𝜒) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒)))))
17 nic-dfim 1585 . . . . 5 ((((𝜓𝜒) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒))) ⊼ ((𝜓𝜒) → (𝜑𝜒))) ⊼ ((((𝜓𝜒) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒))) ⊼ ((𝜓𝜒) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒)))) ⊼ (((𝜓𝜒) → (𝜑𝜒)) ⊼ ((𝜓𝜒) → (𝜑𝜒)))))
1817nic-bi1 1604 . . . 4 (((𝜓𝜒) ⊼ ((𝜑𝜒) ⊼ (𝜑𝜒))) ⊼ (((𝜓𝜒) → (𝜑𝜒)) ⊼ ((𝜓𝜒) → (𝜑𝜒))))
1916, 18nic-ich 1601 . . 3 ((𝜑 ⊼ (𝜓𝜓)) ⊼ (((𝜓𝜒) → (𝜑𝜒)) ⊼ ((𝜓𝜒) → (𝜑𝜒))))
202, 19nic-ich 1601 . 2 ((𝜑𝜓) ⊼ (((𝜓𝜒) → (𝜑𝜒)) ⊼ ((𝜓𝜒) → (𝜑𝜒))))
21 nic-dfim 1585 . . 3 ((((𝜑𝜓) ⊼ (((𝜓𝜒) → (𝜑𝜒)) ⊼ ((𝜓𝜒) → (𝜑𝜒)))) ⊼ ((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒)))) ⊼ ((((𝜑𝜓) ⊼ (((𝜓𝜒) → (𝜑𝜒)) ⊼ ((𝜓𝜒) → (𝜑𝜒)))) ⊼ ((𝜑𝜓) ⊼ (((𝜓𝜒) → (𝜑𝜒)) ⊼ ((𝜓𝜒) → (𝜑𝜒))))) ⊼ (((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒))) ⊼ ((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒))))))
2221nic-bi1 1604 . 2 (((𝜑𝜓) ⊼ (((𝜓𝜒) → (𝜑𝜒)) ⊼ ((𝜓𝜒) → (𝜑𝜒)))) ⊼ (((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒))) ⊼ ((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒)))))
2320, 22nic-mp 1587 1 ((𝜑𝜓) → ((𝜓𝜒) → (𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnan 1439
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 196  df-or 384  df-an 385  df-nan 1440
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator