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