Metamath Proof Explorer

Theorem meran3

Description: A single axiom for propositional calculus discovered by C. A. Meredith. (Contributed by Anthony Hart, 13-Aug-2011)

Ref Expression
Assertion meran3 ⊢ ¬ ¬ ¬ φ ∨ ψ ∨ χ ∨ θ ∨ τ ∨ ¬ ¬ χ ∨ φ ∨ τ ∨ θ ∨ φ

Proof

Step Hyp Ref Expression
1 pm2.3 ⊢ χ ∨ θ ∨ τ → χ ∨ τ ∨ θ
2 1 imim2i ⊢ ¬ φ ∨ ψ → χ ∨ θ ∨ τ → ¬ φ ∨ ψ → χ ∨ τ ∨ θ
3 pm1.5 ⊢ χ ∨ τ ∨ θ → τ ∨ χ ∨ θ
4 2 3 syl6 ⊢ ¬ φ ∨ ψ → χ ∨ θ ∨ τ → ¬ φ ∨ ψ → τ ∨ χ ∨ θ
5 imor ⊢ ¬ φ ∨ ψ → χ ∨ θ ∨ τ ↔ ¬ ¬ φ ∨ ψ ∨ χ ∨ θ ∨ τ
6 imor ⊢ ¬ φ ∨ ψ → τ ∨ χ ∨ θ ↔ ¬ ¬ φ ∨ ψ ∨ τ ∨ χ ∨ θ
7 4 5 6 3imtr3i ⊢ ¬ ¬ φ ∨ ψ ∨ χ ∨ θ ∨ τ → ¬ ¬ φ ∨ ψ ∨ τ ∨ χ ∨ θ
8 meran1 ⊢ ¬ ¬ ¬ φ ∨ ψ ∨ τ ∨ χ ∨ θ ∨ ¬ ¬ χ ∨ φ ∨ τ ∨ θ ∨ φ
9 8 imorri ⊢ ¬ ¬ φ ∨ ψ ∨ τ ∨ χ ∨ θ → ¬ ¬ χ ∨ φ ∨ τ ∨ θ ∨ φ
10 7 9 syl ⊢ ¬ ¬ φ ∨ ψ ∨ χ ∨ θ ∨ τ → ¬ ¬ χ ∨ φ ∨ τ ∨ θ ∨ φ
11 10 imori ⊢ ¬ ¬ ¬ φ ∨ ψ ∨ χ ∨ θ ∨ τ ∨ ¬ ¬ χ ∨ φ ∨ τ ∨ θ ∨ φ