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 ¬ ¬ ¬ φ ψ χ θ τ ¬ ¬ τ θ χ φ θ