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

Theorem rblem4 1768
Description: Used to rederive the Lukasiewicz axioms from Russell-Bernays'. (Contributed by Anthony Hart, 18-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
rblem4.1 𝜑𝜃)
rblem4.2 𝜓𝜏)
rblem4.3 𝜒𝜂)
Assertion
Ref Expression
rblem4 (¬ ((𝜑𝜓) ∨ 𝜒) ∨ ((𝜂𝜏) ∨ 𝜃))

Proof of Theorem rblem4
StepHypRef Expression
1 rblem4.3 . . . 4 𝜒𝜂)
2 rblem4.2 . . . 4 𝜓𝜏)
31, 2rblem1 1765 . . 3 (¬ (𝜒𝜓) ∨ (𝜂𝜏))
4 rblem4.1 . . 3 𝜑𝜃)
53, 4rblem1 1765 . 2 (¬ ((𝜒𝜓) ∨ 𝜑) ∨ ((𝜂𝜏) ∨ 𝜃))
6 rb-ax2 1761 . . . 4 (¬ (𝜑 ∨ (𝜒𝜓)) ∨ ((𝜒𝜓) ∨ 𝜑))
7 rb-ax2 1761 . . . . . 6 (¬ (𝜓𝜒) ∨ (𝜒𝜓))
8 rb-ax1 1760 . . . . . 6 (¬ (¬ (𝜓𝜒) ∨ (𝜒𝜓)) ∨ (¬ (𝜑 ∨ (𝜓𝜒)) ∨ (𝜑 ∨ (𝜒𝜓))))
97, 8anmp 1759 . . . . 5 (¬ (𝜑 ∨ (𝜓𝜒)) ∨ (𝜑 ∨ (𝜒𝜓)))
10 rb-ax2 1761 . . . . 5 (¬ ((𝜓𝜒) ∨ 𝜑) ∨ (𝜑 ∨ (𝜓𝜒)))
119, 10rbsyl 1764 . . . 4 (¬ ((𝜓𝜒) ∨ 𝜑) ∨ (𝜑 ∨ (𝜒𝜓)))
126, 11rbsyl 1764 . . 3 (¬ ((𝜓𝜒) ∨ 𝜑) ∨ ((𝜒𝜓) ∨ 𝜑))
13 rb-ax4 1763 . . . 4 (¬ (((𝜓𝜒) ∨ 𝜑) ∨ ((𝜓𝜒) ∨ 𝜑)) ∨ ((𝜓𝜒) ∨ 𝜑))
14 rb-ax2 1761 . . . . . 6 (¬ (𝜑 ∨ (𝜓𝜒)) ∨ ((𝜓𝜒) ∨ 𝜑))
15 rblem2 1766 . . . . . 6 (¬ (𝜑𝜓) ∨ (𝜑 ∨ (𝜓𝜒)))
1614, 15rbsyl 1764 . . . . 5 (¬ (𝜑𝜓) ∨ ((𝜓𝜒) ∨ 𝜑))
17 rb-ax3 1762 . . . . . 6 𝜒 ∨ (𝜓𝜒))
18 rblem2 1766 . . . . . 6 (¬ (¬ 𝜒 ∨ (𝜓𝜒)) ∨ (¬ 𝜒 ∨ ((𝜓𝜒) ∨ 𝜑)))
1917, 18anmp 1759 . . . . 5 𝜒 ∨ ((𝜓𝜒) ∨ 𝜑))
2016, 19rblem1 1765 . . . 4 (¬ ((𝜑𝜓) ∨ 𝜒) ∨ (((𝜓𝜒) ∨ 𝜑) ∨ ((𝜓𝜒) ∨ 𝜑)))
2113, 20rbsyl 1764 . . 3 (¬ ((𝜑𝜓) ∨ 𝜒) ∨ ((𝜓𝜒) ∨ 𝜑))
2212, 21rbsyl 1764 . 2 (¬ ((𝜑𝜓) ∨ 𝜒) ∨ ((𝜒𝜓) ∨ 𝜑))
235, 22rbsyl 1764 1 (¬ ((𝜑𝜓) ∨ 𝜒) ∨ ((𝜂𝜏) ∨ 𝜃))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 847
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 210  df-an 400  df-or 848
This theorem is referenced by:  re2luk1  1773
  Copyright terms: Public domain W3C validator