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