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 ( ( 𝜑 ⊼ ( 𝜓𝜒 ) ) ⊼ ( ( 𝜑 ⊼ ( 𝜓𝜒 ) ) ⊼ ( ( 𝜃𝜒 ) ⊼ ( ( 𝜒𝜃 ) ⊼ ( 𝜑𝜃 ) ) ) ) )