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