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