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

Theorem rblem5 1753
Description: Used to rederive the Lukasiewicz axioms from Russell-Bernays'. (Contributed by Anthony Hart, 19-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
rblem5 (¬ (¬ ¬ 𝜑𝜓) ∨ (¬ ¬ 𝜓𝜑))

Proof of Theorem rblem5
StepHypRef Expression
1 rb-ax2 1745 . 2 (¬ (𝜑 ∨ ¬ ¬ 𝜓) ∨ (¬ ¬ 𝜓𝜑))
2 rb-ax4 1747 . . . . 5 (¬ (𝜑𝜑) ∨ 𝜑)
3 rb-ax3 1746 . . . . 5 𝜑 ∨ (𝜑𝜑))
42, 3rbsyl 1748 . . . 4 𝜑𝜑)
5 rb-ax4 1747 . . . . . . 7 (¬ (¬ ¬ 𝜑 ∨ ¬ ¬ 𝜑) ∨ ¬ ¬ 𝜑)
6 rb-ax3 1746 . . . . . . 7 (¬ ¬ ¬ 𝜑 ∨ (¬ ¬ 𝜑 ∨ ¬ ¬ 𝜑))
75, 6rbsyl 1748 . . . . . 6 (¬ ¬ ¬ 𝜑 ∨ ¬ ¬ 𝜑)
8 rb-ax2 1745 . . . . . 6 (¬ (¬ ¬ ¬ 𝜑 ∨ ¬ ¬ 𝜑) ∨ (¬ ¬ 𝜑 ∨ ¬ ¬ ¬ 𝜑))
97, 8anmp 1743 . . . . 5 (¬ ¬ 𝜑 ∨ ¬ ¬ ¬ 𝜑)
109, 4rblem1 1749 . . . 4 (¬ (¬ 𝜑𝜑) ∨ (¬ ¬ ¬ 𝜑𝜑))
114, 10anmp 1743 . . 3 (¬ ¬ ¬ 𝜑𝜑)
12 rb-ax4 1747 . . . . 5 (¬ (¬ 𝜓 ∨ ¬ 𝜓) ∨ ¬ 𝜓)
13 rb-ax3 1746 . . . . 5 (¬ ¬ 𝜓 ∨ (¬ 𝜓 ∨ ¬ 𝜓))
1412, 13rbsyl 1748 . . . 4 (¬ ¬ 𝜓 ∨ ¬ 𝜓)
15 rb-ax2 1745 . . . 4 (¬ (¬ ¬ 𝜓 ∨ ¬ 𝜓) ∨ (¬ 𝜓 ∨ ¬ ¬ 𝜓))
1614, 15anmp 1743 . . 3 𝜓 ∨ ¬ ¬ 𝜓)
1711, 16rblem1 1749 . 2 (¬ (¬ ¬ 𝜑𝜓) ∨ (𝜑 ∨ ¬ ¬ 𝜓))
181, 17rbsyl 1748 1 (¬ (¬ ¬ 𝜑𝜓) ∨ (¬ ¬ 𝜓𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 841
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 208  df-an 397  df-or 842
This theorem is referenced by:  rblem6  1754  rblem7  1755
  Copyright terms: Public domain W3C validator