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