Metamath Proof Explorer

Theorem waj-ax

Description: A single axiom for propositional calculus discovered by Mordchaj Wajsberg (Logical Works, Polish Academy of Sciences, 1977). See: Fitelson,Some recent results in algebra and logical calculi obtained using automated reasoning, 2003 (axiom W on slide 8). (Contributed by Anthony Hart, 13-Aug-2011)

Ref Expression
Assertion waj-ax ⊢φ⊼ψ⊼χ⊼θ⊼χ⊼φ⊼θ⊼φ⊼θ⊼φ⊼φ⊼ψ

Proof

Step Hyp Ref Expression
1 nannan ⊢φ⊼ψ⊼χ↔φ→ψ∧χ
2 simpr ⊢ψ∧χ→χ
3 2 imim2i ⊢φ→ψ∧χ→φ→χ
4 pm2.27 ⊢φ→φ→χ→χ
5 4 anim2d ⊢φ→θ∧φ→χ→θ∧χ
6 5 expdimp ⊢φ∧θ→φ→χ→θ∧χ
7 3 6 syl5com ⊢φ→ψ∧χ→φ∧θ→θ∧χ
8 7 con3d ⊢φ→ψ∧χ→¬θ∧χ→¬φ∧θ
9 df-nan ⊢θ⊼χ↔¬θ∧χ
10 df-nan ⊢φ⊼θ↔¬φ∧θ
11 8 9 10 3imtr4g ⊢φ→ψ∧χ→θ⊼χ→φ⊼θ
12 nanim ⊢θ⊼χ→φ⊼θ↔θ⊼χ⊼φ⊼θ⊼φ⊼θ
13 11 12 sylib ⊢φ→ψ∧χ→θ⊼χ⊼φ⊼θ⊼φ⊼θ
14 pm3.21 ⊢ψ→φ→φ∧ψ
15 14 adantr ⊢ψ∧χ→φ→φ∧ψ
16 15 com12 ⊢φ→ψ∧χ→φ∧ψ
17 16 a2i ⊢φ→ψ∧χ→φ→φ∧ψ
18 nannan ⊢φ⊼φ⊼ψ↔φ→φ∧ψ
19 17 18 sylibr ⊢φ→ψ∧χ→φ⊼φ⊼ψ
20 13 19 jca ⊢φ→ψ∧χ→θ⊼χ⊼φ⊼θ⊼φ⊼θ∧φ⊼φ⊼ψ
21 1 20 sylbi ⊢φ⊼ψ⊼χ→θ⊼χ⊼φ⊼θ⊼φ⊼θ∧φ⊼φ⊼ψ
22 nannan ⊢φ⊼ψ⊼χ⊼θ⊼χ⊼φ⊼θ⊼φ⊼θ⊼φ⊼φ⊼ψ↔φ⊼ψ⊼χ→θ⊼χ⊼φ⊼θ⊼φ⊼θ∧φ⊼φ⊼ψ
23 21 22 mpbir ⊢φ⊼ψ⊼χ⊼θ⊼χ⊼φ⊼θ⊼φ⊼θ⊼φ⊼φ⊼ψ