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