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