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 ⊢¬φ∨ψ