Metamath Proof Explorer

Theorem meran1

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

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

Proof

Step Hyp Ref Expression
1 orc ⊢ ¬ φ → ¬ φ ∨ ψ
2 olc ⊢ ψ → ¬ φ ∨ ψ
3 1 2 ja ⊢ φ → ψ → ¬ φ ∨ ψ
4 3 imim1i ⊢ ¬ φ ∨ ψ → χ ∨ θ ∨ τ → φ → ψ → χ ∨ θ ∨ τ
5 pm2.24 ⊢ θ → ¬ θ → φ
6 idd ⊢ θ → φ → φ
7 5 6 jaod ⊢ θ → ¬ θ ∨ φ → φ
8 7 com12 ⊢ ¬ θ ∨ φ → θ → φ
9 pm1.5 ⊢ ¬ φ → ψ ∨ χ ∨ θ ∨ τ → χ ∨ ¬ φ → ψ ∨ θ ∨ τ
10 pm2.3 ⊢ ¬ φ → ψ ∨ θ ∨ τ → ¬ φ → ψ ∨ τ ∨ θ
11 pm1.5 ⊢ ¬ φ → ψ ∨ τ ∨ θ → τ ∨ ¬ φ → ψ ∨ θ
12 pm2.21 ⊢ ¬ φ → φ → ψ
13 jcn ⊢ θ → ¬ φ → ¬ θ → φ
14 12 13 imim12i ⊢ φ → ψ → θ → ¬ φ → ¬ φ → ¬ θ → φ
15 14 pm2.43d ⊢ φ → ψ → θ → ¬ φ → ¬ θ → φ
16 15 con4d ⊢ φ → ψ → θ → θ → φ → φ
17 imor ⊢ φ → ψ → θ ↔ ¬ φ → ψ ∨ θ
18 imor ⊢ θ → φ → φ ↔ ¬ θ → φ ∨ φ
19 16 17 18 3imtr3i ⊢ ¬ φ → ψ ∨ θ → ¬ θ → φ ∨ φ
20 19 orim2i ⊢ τ ∨ ¬ φ → ψ ∨ θ → τ ∨ ¬ θ → φ ∨ φ
21 pm1.5 ⊢ τ ∨ ¬ θ → φ ∨ φ → ¬ θ → φ ∨ τ ∨ φ
22 10 11 20 21 4syl ⊢ ¬ φ → ψ ∨ θ ∨ τ → ¬ θ → φ ∨ τ ∨ φ
23 22 orim2i ⊢ χ ∨ ¬ φ → ψ ∨ θ ∨ τ → χ ∨ ¬ θ → φ ∨ τ ∨ φ
24 pm1.5 ⊢ χ ∨ ¬ θ → φ ∨ τ ∨ φ → ¬ θ → φ ∨ χ ∨ τ ∨ φ
25 9 23 24 3syl ⊢ ¬ φ → ψ ∨ χ ∨ θ ∨ τ → ¬ θ → φ ∨ χ ∨ τ ∨ φ
26 imor ⊢ φ → ψ → χ ∨ θ ∨ τ ↔ ¬ φ → ψ ∨ χ ∨ θ ∨ τ
27 imor ⊢ θ → φ → χ ∨ τ ∨ φ ↔ ¬ θ → φ ∨ χ ∨ τ ∨ φ
28 25 26 27 3imtr4i ⊢ φ → ψ → χ ∨ θ ∨ τ → θ → φ → χ ∨ τ ∨ φ
29 4 8 28 syl2im ⊢ ¬ φ ∨ ψ → χ ∨ θ ∨ τ → ¬ θ ∨ φ → χ ∨ τ ∨ φ
30 imor ⊢ ¬ φ ∨ ψ → χ ∨ θ ∨ τ ↔ ¬ ¬ φ ∨ ψ ∨ χ ∨ θ ∨ τ
31 imor ⊢ ¬ θ ∨ φ → χ ∨ τ ∨ φ ↔ ¬ ¬ θ ∨ φ ∨ χ ∨ τ ∨ φ
32 29 30 31 3imtr3i ⊢ ¬ ¬ φ ∨ ψ ∨ χ ∨ θ ∨ τ → ¬ ¬ θ ∨ φ ∨ χ ∨ τ ∨ φ
33 32 imori ⊢ ¬ ¬ ¬ φ ∨ ψ ∨ χ ∨ θ ∨ τ ∨ ¬ ¬ θ ∨ φ ∨ χ ∨ τ ∨ φ