Metamath Proof Explorer

Theorem lukshef-ax2

Description: A single axiom for propositional calculus discovered by Jan Lukasiewicz. See: Fitelson,Some recent results in algebra and logical calculi obtained using automated reasoning, 2003 (axiom L2 on slide 8). (Contributed by Anthony Hart, 14-Aug-2011)

Ref Expression
Assertion lukshef-ax2 ⊢ φ ⊼ ψ ⊼ χ ⊼ φ ⊼ χ ⊼ φ ⊼ θ ⊼ ψ ⊼ φ ⊼ θ ⊼ φ ⊼ θ

Proof

Step Hyp Ref Expression
1 nannan ⊢ φ ⊼ ψ ⊼ χ ↔ φ → ψ ∧ χ
2 1 biimpi ⊢ φ ⊼ ψ ⊼ χ → φ → ψ ∧ χ
3 simpr ⊢ ψ ∧ χ → χ
4 3 imim2i ⊢ φ → ψ ∧ χ → φ → χ
5 simpl ⊢ ψ ∧ χ → ψ
6 5 imim2i ⊢ φ → ψ ∧ χ → φ → ψ
7 pm2.27 ⊢ φ → φ → ψ → ψ
8 7 anim2d ⊢ φ → θ ∧ φ → ψ → θ ∧ ψ
9 8 expdimp ⊢ φ ∧ θ → φ → ψ → θ ∧ ψ
10 6 9 syl5com ⊢ φ → ψ ∧ χ → φ ∧ θ → θ ∧ ψ
11 ancr ⊢ φ → χ → φ → χ ∧ φ
12 11 anim1i ⊢ φ → χ ∧ φ ∧ θ → θ ∧ ψ → φ → χ ∧ φ ∧ φ ∧ θ → θ ∧ ψ
13 4 10 12 syl2anc ⊢ φ → ψ ∧ χ → φ → χ ∧ φ ∧ φ ∧ θ → θ ∧ ψ
14 con3 ⊢ φ ∧ θ → θ ∧ ψ → ¬ θ ∧ ψ → ¬ φ ∧ θ
15 df-nan ⊢ θ ⊼ ψ ↔ ¬ θ ∧ ψ
16 df-nan ⊢ φ ⊼ θ ↔ ¬ φ ∧ θ
17 14 15 16 3imtr4g ⊢ φ ∧ θ → θ ∧ ψ → θ ⊼ ψ → φ ⊼ θ
18 17 anim2i ⊢ φ → χ ∧ φ ∧ φ ∧ θ → θ ∧ ψ → φ → χ ∧ φ ∧ θ ⊼ ψ → φ ⊼ θ
19 nannan ⊢ φ ⊼ χ ⊼ φ ↔ φ → χ ∧ φ
20 19 biimpri ⊢ φ → χ ∧ φ → φ ⊼ χ ⊼ φ
21 nanim ⊢ θ ⊼ ψ → φ ⊼ θ ↔ θ ⊼ ψ ⊼ φ ⊼ θ ⊼ φ ⊼ θ
22 21 biimpi ⊢ θ ⊼ ψ → φ ⊼ θ → θ ⊼ ψ ⊼ φ ⊼ θ ⊼ φ ⊼ θ
23 20 22 anim12i ⊢ φ → χ ∧ φ ∧ θ ⊼ ψ → φ ⊼ θ → φ ⊼ χ ⊼ φ ∧ θ ⊼ ψ ⊼ φ ⊼ θ ⊼ φ ⊼ θ
24 2 13 18 23 4syl ⊢ φ ⊼ ψ ⊼ χ → φ ⊼ χ ⊼ φ ∧ θ ⊼ ψ ⊼ φ ⊼ θ ⊼ φ ⊼ θ
25 nannan ⊢ φ ⊼ ψ ⊼ χ ⊼ φ ⊼ χ ⊼ φ ⊼ θ ⊼ ψ ⊼ φ ⊼ θ ⊼ φ ⊼ θ ↔ φ ⊼ ψ ⊼ χ → φ ⊼ χ ⊼ φ ∧ θ ⊼ ψ ⊼ φ ⊼ θ ⊼ φ ⊼ θ
26 24 25 mpbir ⊢ φ ⊼ ψ ⊼ χ ⊼ φ ⊼ χ ⊼ φ ⊼ θ ⊼ ψ ⊼ φ ⊼ θ ⊼ φ ⊼ θ