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 ⊢ φ ⊼ ψ ⊼ χ ⊼ θ ⊼ χ ⊼ φ ⊼ θ ⊼ φ ⊼ θ ⊼ φ ⊼ φ ⊼ ψ