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

Theorem rblem4 1683
 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 1680 . . 3 (¬ (𝜒𝜓) ∨ (𝜂𝜏))
4 rblem4.1 . . 3 𝜑𝜃)
53, 4rblem1 1680 . 2 (¬ ((𝜒𝜓) ∨ 𝜑) ∨ ((𝜂𝜏) ∨ 𝜃))
6 rb-ax2 1676 . . . 4 (¬ (𝜑 ∨ (𝜒𝜓)) ∨ ((𝜒𝜓) ∨ 𝜑))
7 rb-ax2 1676 . . . . . 6 (¬ (𝜓𝜒) ∨ (𝜒𝜓))
8 rb-ax1 1675 . . . . . 6 (¬ (¬ (𝜓𝜒) ∨ (𝜒𝜓)) ∨ (¬ (𝜑 ∨ (𝜓𝜒)) ∨ (𝜑 ∨ (𝜒𝜓))))
97, 8anmp 1674 . . . . 5 (¬ (𝜑 ∨ (𝜓𝜒)) ∨ (𝜑 ∨ (𝜒𝜓)))
10 rb-ax2 1676 . . . . 5 (¬ ((𝜓𝜒) ∨ 𝜑) ∨ (𝜑 ∨ (𝜓𝜒)))
119, 10rbsyl 1679 . . . 4 (¬ ((𝜓𝜒) ∨ 𝜑) ∨ (𝜑 ∨ (𝜒𝜓)))
126, 11rbsyl 1679 . . 3 (¬ ((𝜓𝜒) ∨ 𝜑) ∨ ((𝜒𝜓) ∨ 𝜑))
13 rb-ax4 1678 . . . 4 (¬ (((𝜓𝜒) ∨ 𝜑) ∨ ((𝜓𝜒) ∨ 𝜑)) ∨ ((𝜓𝜒) ∨ 𝜑))
14 rb-ax2 1676 . . . . . 6 (¬ (𝜑 ∨ (𝜓𝜒)) ∨ ((𝜓𝜒) ∨ 𝜑))
15 rblem2 1681 . . . . . 6 (¬ (𝜑𝜓) ∨ (𝜑 ∨ (𝜓𝜒)))
1614, 15rbsyl 1679 . . . . 5 (¬ (𝜑𝜓) ∨ ((𝜓𝜒) ∨ 𝜑))
17 rb-ax3 1677 . . . . . 6 𝜒 ∨ (𝜓𝜒))
18 rblem2 1681 . . . . . 6 (¬ (¬ 𝜒 ∨ (𝜓𝜒)) ∨ (¬ 𝜒 ∨ ((𝜓𝜒) ∨ 𝜑)))
1917, 18anmp 1674 . . . . 5 𝜒 ∨ ((𝜓𝜒) ∨ 𝜑))
2016, 19rblem1 1680 . . . 4 (¬ ((𝜑𝜓) ∨ 𝜒) ∨ (((𝜓𝜒) ∨ 𝜑) ∨ ((𝜓𝜒) ∨ 𝜑)))
2113, 20rbsyl 1679 . . 3 (¬ ((𝜑𝜓) ∨ 𝜒) ∨ ((𝜓𝜒) ∨ 𝜑))
2212, 21rbsyl 1679 . 2 (¬ ((𝜑𝜓) ∨ 𝜒) ∨ ((𝜒𝜓) ∨ 𝜑))
235, 22rbsyl 1679 1 (¬ ((𝜑𝜓) ∨ 𝜒) ∨ ((𝜂𝜏) ∨ 𝜃))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ∨ wo 383 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 385  df-an 386 This theorem is referenced by:  re2luk1  1688
 Copyright terms: Public domain W3C validator