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 syl5bi φ ψ χ ¬ ¬ χ θ ¬ φ θ θ χ
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 syl5bi φ ψ χ θ χ χ θ φ θ
27 nannan φ ψ χ φ ψ χ
28 nannan θ χ χ θ φ θ θ χ χ θ φ θ
29 26 27 28 3imtr4i φ ψ χ θ χ χ θ φ θ
30 29 ancli φ ψ χ φ ψ χ θ χ χ θ φ θ
31 nannan φ ψ χ φ ψ χ θ χ χ θ φ θ φ ψ χ φ ψ χ θ χ χ θ φ θ
32 30 31 mpbir φ ψ χ φ ψ χ θ χ χ θ φ θ