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

Theorem rblem1 1722
 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
rblem1.1 𝜑𝜓)
rblem1.2 𝜒𝜃)
Assertion
Ref Expression
rblem1 (¬ (𝜑𝜒) ∨ (𝜓𝜃))

Proof of Theorem rblem1
StepHypRef Expression
1 rblem1.2 . . 3 𝜒𝜃)
2 rb-ax1 1717 . . 3 (¬ (¬ 𝜒𝜃) ∨ (¬ (𝜓𝜒) ∨ (𝜓𝜃)))
31, 2anmp 1716 . 2 (¬ (𝜓𝜒) ∨ (𝜓𝜃))
4 rb-ax2 1718 . . 3 (¬ (𝜒𝜓) ∨ (𝜓𝜒))
5 rblem1.1 . . . . 5 𝜑𝜓)
6 rb-ax1 1717 . . . . 5 (¬ (¬ 𝜑𝜓) ∨ (¬ (𝜒𝜑) ∨ (𝜒𝜓)))
75, 6anmp 1716 . . . 4 (¬ (𝜒𝜑) ∨ (𝜒𝜓))
8 rb-ax2 1718 . . . 4 (¬ (𝜑𝜒) ∨ (𝜒𝜑))
97, 8rbsyl 1721 . . 3 (¬ (𝜑𝜒) ∨ (𝜒𝜓))
104, 9rbsyl 1721 . 2 (¬ (𝜑𝜒) ∨ (𝜓𝜒))
113, 10rbsyl 1721 1 (¬ (𝜑𝜒) ∨ (𝜓𝜃))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ∨ wo 382 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 This theorem is referenced by:  rblem4  1725  rblem5  1726  re2luk1  1730  re2luk2  1731
 Copyright terms: Public domain W3C validator