Metamath Proof Explorer

Theorem meran2

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

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

Proof

Step Hyp Ref Expression
1 meran1 ⊢ ¬ ¬ ¬ φ ∨ ψ ∨ χ ∨ θ ∨ τ ∨ ¬ ¬ θ ∨ φ ∨ χ ∨ τ ∨ φ
2 1 imorri ⊢ ¬ ¬ φ ∨ ψ ∨ χ ∨ θ ∨ τ → ¬ ¬ θ ∨ φ ∨ χ ∨ τ ∨ φ
3 meran1 ⊢ ¬ ¬ ¬ θ ∨ φ ∨ χ ∨ τ ∨ φ ∨ ¬ ¬ τ ∨ θ ∨ χ ∨ φ ∨ θ
4 3 imorri ⊢ ¬ ¬ θ ∨ φ ∨ χ ∨ τ ∨ φ → ¬ ¬ τ ∨ θ ∨ χ ∨ φ ∨ θ
5 2 4 syl ⊢ ¬ ¬ φ ∨ ψ ∨ χ ∨ θ ∨ τ → ¬ ¬ τ ∨ θ ∨ χ ∨ φ ∨ θ
6 5 imori ⊢ ¬ ¬ ¬ φ ∨ ψ ∨ χ ∨ θ ∨ τ ∨ ¬ ¬ τ ∨ θ ∨ χ ∨ φ ∨ θ