Metamath Proof Explorer

Theorem rblem1

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 rblem1.1 ⊢ ¬ φ ∨ ψ
rblem1.2 ⊢ ¬ χ ∨ θ
Assertion rblem1 ⊢ ¬ φ ∨ χ ∨ ψ ∨ θ

Proof

Step Hyp Ref Expression
1 rblem1.1 ⊢ ¬ φ ∨ ψ
2 rblem1.2 ⊢ ¬ χ ∨ θ
3 rb-ax1 ⊢ ¬ ¬ χ ∨ θ ∨ ¬ ψ ∨ χ ∨ ψ ∨ θ
4 2 3 anmp ⊢ ¬ ψ ∨ χ ∨ ψ ∨ θ
5 rb-ax2 ⊢ ¬ χ ∨ ψ ∨ ψ ∨ χ
6 rb-ax1 ⊢ ¬ ¬ φ ∨ ψ ∨ ¬ χ ∨ φ ∨ χ ∨ ψ
7 1 6 anmp ⊢ ¬ χ ∨ φ ∨ χ ∨ ψ
8 rb-ax2 ⊢ ¬ φ ∨ χ ∨ χ ∨ φ
9 7 8 rbsyl ⊢ ¬ φ ∨ χ ∨ χ ∨ ψ
10 5 9 rbsyl ⊢ ¬ φ ∨ χ ∨ ψ ∨ χ
11 4 10 rbsyl ⊢ ¬ φ ∨ χ ∨ ψ ∨ θ