Metamath Proof Explorer

Theorem rblem6

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.)

Ref Expression
Hypothesis rblem6.1 ⊢ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ ψ ∨ φ
Assertion rblem6 ⊢ ¬ φ ∨ ψ

Proof

Step Hyp Ref Expression
1 rblem6.1 ⊢ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ ψ ∨ φ
2 rb-ax4 ⊢ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ φ ∨ ψ
3 rb-ax3 ⊢ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ φ ∨ ψ
4 2 3 rbsyl ⊢ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ φ ∨ ψ
5 rb-ax2 ⊢ ¬ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ ¬ φ ∨ ψ
6 4 5 anmp ⊢ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ ¬ φ ∨ ψ
7 rblem3 ⊢ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ ψ ∨ φ ∨ ¬ ¬ ¬ φ ∨ ψ
8 6 7 anmp ⊢ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ ψ ∨ φ ∨ ¬ ¬ ¬ φ ∨ ψ
9 rb-ax2 ⊢ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ ψ ∨ φ ∨ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ ψ ∨ φ
10 8 9 anmp ⊢ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ ψ ∨ φ
11 rblem5 ⊢ ¬ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ ψ ∨ φ ∨ ¬ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ ψ ∨ φ ∨ ¬ φ ∨ ψ
12 10 11 anmp ⊢ ¬ ¬ ¬ ¬ φ ∨ ψ ∨ ¬ ¬ ψ ∨ φ ∨ ¬ φ ∨ ψ
13 1 12 anmp ⊢ ¬ φ ∨ ψ