Metamath Proof Explorer

Theorem arg-ax

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

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

Proof

Step Hyp Ref Expression
1 df-nan ⊢ θ ⊼ χ ↔ ¬ θ ∧ χ
2 pm4.57 ⊢ ¬ ¬ χ ∧ θ ∧ ¬ φ ∧ θ ↔ χ ∧ θ ∨ φ ∧ θ
3 orel2 ⊢ ¬ φ → χ ∨ φ → χ
4 3 com12 ⊢ χ ∨ φ → ¬ φ → χ
5 simpr ⊢ ψ ∧ χ → χ
6 5 a1i ⊢ χ ∨ φ → ψ ∧ χ → χ
7 4 6 jad ⊢ χ ∨ φ → φ → ψ ∧ χ → χ
8 7 com12 ⊢ φ → ψ ∧ χ → χ ∨ φ → χ
9 pm3.45 ⊢ χ → χ → χ ∧ θ → χ ∧ θ
10 pm3.45 ⊢ φ → χ → φ ∧ θ → χ ∧ θ
11 9 10 anim12i ⊢ χ → χ ∧ φ → χ → χ ∧ θ → χ ∧ θ ∧ φ ∧ θ → χ ∧ θ
12 jaob ⊢ χ ∨ φ → χ ↔ χ → χ ∧ φ → χ
13 jaob ⊢ χ ∧ θ ∨ φ ∧ θ → χ ∧ θ ↔ χ ∧ θ → χ ∧ θ ∧ φ ∧ θ → χ ∧ θ
14 11 12 13 3imtr4i ⊢ χ ∨ φ → χ → χ ∧ θ ∨ φ ∧ θ → χ ∧ θ
15 8 14 syl ⊢ φ → ψ ∧ χ → χ ∧ θ ∨ φ ∧ θ → χ ∧ θ
16 pm3.22 ⊢ χ ∧ θ → θ ∧ χ
17 15 16 syl6 ⊢ φ → ψ ∧ χ → χ ∧ θ ∨ φ ∧ θ → θ ∧ χ
18 2 17 biimtrid ⊢ φ → ψ ∧ χ → ¬ ¬ χ ∧ θ ∧ ¬ φ ∧ θ → θ ∧ χ
19 18 con1d ⊢ φ → ψ ∧ χ → ¬ θ ∧ χ → ¬ χ ∧ θ ∧ ¬ φ ∧ θ
20 df-nan ⊢ χ ⊼ θ ↔ ¬ χ ∧ θ
21 20 biimpri ⊢ ¬ χ ∧ θ → χ ⊼ θ
22 df-nan ⊢ φ ⊼ θ ↔ ¬ φ ∧ θ
23 22 biimpri ⊢ ¬ φ ∧ θ → φ ⊼ θ
24 21 23 anim12i ⊢ ¬ χ ∧ θ ∧ ¬ φ ∧ θ → χ ⊼ θ ∧ φ ⊼ θ
25 19 24 syl6 ⊢ φ → ψ ∧ χ → ¬ θ ∧ χ → χ ⊼ θ ∧ φ ⊼ θ
26 1 25 biimtrid ⊢ φ → ψ ∧ χ → θ ⊼ χ → χ ⊼ θ ∧ φ ⊼ θ
27 nannan ⊢ φ ⊼ ψ ⊼ χ ↔ φ → ψ ∧ χ
28 nannan ⊢ θ ⊼ χ ⊼ χ ⊼ θ ⊼ φ ⊼ θ ↔ θ ⊼ χ → χ ⊼ θ ∧ φ ⊼ θ
29 26 27 28 3imtr4i ⊢ φ ⊼ ψ ⊼ χ → θ ⊼ χ ⊼ χ ⊼ θ ⊼ φ ⊼ θ
30 29 ancli ⊢ φ ⊼ ψ ⊼ χ → φ ⊼ ψ ⊼ χ ∧ θ ⊼ χ ⊼ χ ⊼ θ ⊼ φ ⊼ θ
31 nannan ⊢ φ ⊼ ψ ⊼ χ ⊼ φ ⊼ ψ ⊼ χ ⊼ θ ⊼ χ ⊼ χ ⊼ θ ⊼ φ ⊼ θ ↔ φ ⊼ ψ ⊼ χ → φ ⊼ ψ ⊼ χ ∧ θ ⊼ χ ⊼ χ ⊼ θ ⊼ φ ⊼ θ
32 30 31 mpbir ⊢ φ ⊼ ψ ⊼ χ ⊼ φ ⊼ ψ ⊼ χ ⊼ θ ⊼ χ ⊼ χ ⊼ θ ⊼ φ ⊼ θ