Metamath Proof Explorer

Theorem rblem4

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

Ref Expression
Hypotheses rblem4.1 ⊢ ¬ φ ∨ θ
rblem4.2 ⊢ ¬ ψ ∨ τ
rblem4.3 ⊢ ¬ χ ∨ η
Assertion rblem4 ⊢ ¬ φ ∨ ψ ∨ χ ∨ η ∨ τ ∨ θ

Proof

Step Hyp Ref Expression
1 rblem4.1 ⊢ ¬ φ ∨ θ
2 rblem4.2 ⊢ ¬ ψ ∨ τ
3 rblem4.3 ⊢ ¬ χ ∨ η
4 3 2 rblem1 ⊢ ¬ χ ∨ ψ ∨ η ∨ τ
5 4 1 rblem1 ⊢ ¬ χ ∨ ψ ∨ φ ∨ η ∨ τ ∨ θ
6 rb-ax2 ⊢ ¬ φ ∨ χ ∨ ψ ∨ χ ∨ ψ ∨ φ
7 rb-ax2 ⊢ ¬ ψ ∨ χ ∨ χ ∨ ψ
8 rb-ax1 ⊢ ¬ ¬ ψ ∨ χ ∨ χ ∨ ψ ∨ ¬ φ ∨ ψ ∨ χ ∨ φ ∨ χ ∨ ψ
9 7 8 anmp ⊢ ¬ φ ∨ ψ ∨ χ ∨ φ ∨ χ ∨ ψ
10 rb-ax2 ⊢ ¬ ψ ∨ χ ∨ φ ∨ φ ∨ ψ ∨ χ
11 9 10 rbsyl ⊢ ¬ ψ ∨ χ ∨ φ ∨ φ ∨ χ ∨ ψ
12 6 11 rbsyl ⊢ ¬ ψ ∨ χ ∨ φ ∨ χ ∨ ψ ∨ φ
13 rb-ax4 ⊢ ¬ ψ ∨ χ ∨ φ ∨ ψ ∨ χ ∨ φ ∨ ψ ∨ χ ∨ φ
14 rb-ax2 ⊢ ¬ φ ∨ ψ ∨ χ ∨ ψ ∨ χ ∨ φ
15 rblem2 ⊢ ¬ φ ∨ ψ ∨ φ ∨ ψ ∨ χ
16 14 15 rbsyl ⊢ ¬ φ ∨ ψ ∨ ψ ∨ χ ∨ φ
17 rb-ax3 ⊢ ¬ χ ∨ ψ ∨ χ
18 rblem2 ⊢ ¬ ¬ χ ∨ ψ ∨ χ ∨ ¬ χ ∨ ψ ∨ χ ∨ φ
19 17 18 anmp ⊢ ¬ χ ∨ ψ ∨ χ ∨ φ
20 16 19 rblem1 ⊢ ¬ φ ∨ ψ ∨ χ ∨ ψ ∨ χ ∨ φ ∨ ψ ∨ χ ∨ φ
21 13 20 rbsyl ⊢ ¬ φ ∨ ψ ∨ χ ∨ ψ ∨ χ ∨ φ
22 12 21 rbsyl ⊢ ¬ φ ∨ ψ ∨ χ ∨ χ ∨ ψ ∨ φ
23 5 22 rbsyl ⊢ ¬ φ ∨ ψ ∨ χ ∨ η ∨ τ ∨ θ