Users' Mathboxes Mathbox for Anthony Hart < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  arg-ax Structured version   Visualization version   GIF version

Theorem arg-ax 33838
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.)
Assertion
Ref Expression
arg-ax ((𝜑 ⊼ (𝜓𝜒)) ⊼ ((𝜑 ⊼ (𝜓𝜒)) ⊼ ((𝜃𝜒) ⊼ ((𝜒𝜃) ⊼ (𝜑𝜃)))))

Proof of Theorem arg-ax
StepHypRef Expression
1 df-nan 1483 . . . . 5 ((𝜃𝜒) ↔ ¬ (𝜃𝜒))
2 pm4.57 988 . . . . . . . 8 (¬ (¬ (𝜒𝜃) ∧ ¬ (𝜑𝜃)) ↔ ((𝜒𝜃) ∨ (𝜑𝜃)))
3 orel2 888 . . . . . . . . . . . . 13 𝜑 → ((𝜒𝜑) → 𝜒))
43com12 32 . . . . . . . . . . . 12 ((𝜒𝜑) → (¬ 𝜑𝜒))
5 simpr 488 . . . . . . . . . . . . 13 ((𝜓𝜒) → 𝜒)
65a1i 11 . . . . . . . . . . . 12 ((𝜒𝜑) → ((𝜓𝜒) → 𝜒))
74, 6jad 190 . . . . . . . . . . 11 ((𝜒𝜑) → ((𝜑 → (𝜓𝜒)) → 𝜒))
87com12 32 . . . . . . . . . 10 ((𝜑 → (𝜓𝜒)) → ((𝜒𝜑) → 𝜒))
9 pm3.45 624 . . . . . . . . . . . 12 ((𝜒𝜒) → ((𝜒𝜃) → (𝜒𝜃)))
10 pm3.45 624 . . . . . . . . . . . 12 ((𝜑𝜒) → ((𝜑𝜃) → (𝜒𝜃)))
119, 10anim12i 615 . . . . . . . . . . 11 (((𝜒𝜒) ∧ (𝜑𝜒)) → (((𝜒𝜃) → (𝜒𝜃)) ∧ ((𝜑𝜃) → (𝜒𝜃))))
12 jaob 959 . . . . . . . . . . 11 (((𝜒𝜑) → 𝜒) ↔ ((𝜒𝜒) ∧ (𝜑𝜒)))
13 jaob 959 . . . . . . . . . . 11 ((((𝜒𝜃) ∨ (𝜑𝜃)) → (𝜒𝜃)) ↔ (((𝜒𝜃) → (𝜒𝜃)) ∧ ((𝜑𝜃) → (𝜒𝜃))))
1411, 12, 133imtr4i 295 . . . . . . . . . 10 (((𝜒𝜑) → 𝜒) → (((𝜒𝜃) ∨ (𝜑𝜃)) → (𝜒𝜃)))
158, 14syl 17 . . . . . . . . 9 ((𝜑 → (𝜓𝜒)) → (((𝜒𝜃) ∨ (𝜑𝜃)) → (𝜒𝜃)))
16 pm3.22 463 . . . . . . . . 9 ((𝜒𝜃) → (𝜃𝜒))
1715, 16syl6 35 . . . . . . . 8 ((𝜑 → (𝜓𝜒)) → (((𝜒𝜃) ∨ (𝜑𝜃)) → (𝜃𝜒)))
182, 17syl5bi 245 . . . . . . 7 ((𝜑 → (𝜓𝜒)) → (¬ (¬ (𝜒𝜃) ∧ ¬ (𝜑𝜃)) → (𝜃𝜒)))
1918con1d 147 . . . . . 6 ((𝜑 → (𝜓𝜒)) → (¬ (𝜃𝜒) → (¬ (𝜒𝜃) ∧ ¬ (𝜑𝜃))))
20 df-nan 1483 . . . . . . . 8 ((𝜒𝜃) ↔ ¬ (𝜒𝜃))
2120biimpri 231 . . . . . . 7 (¬ (𝜒𝜃) → (𝜒𝜃))
22 df-nan 1483 . . . . . . . 8 ((𝜑𝜃) ↔ ¬ (𝜑𝜃))
2322biimpri 231 . . . . . . 7 (¬ (𝜑𝜃) → (𝜑𝜃))
2421, 23anim12i 615 . . . . . 6 ((¬ (𝜒𝜃) ∧ ¬ (𝜑𝜃)) → ((𝜒𝜃) ∧ (𝜑𝜃)))
2519, 24syl6 35 . . . . 5 ((𝜑 → (𝜓𝜒)) → (¬ (𝜃𝜒) → ((𝜒𝜃) ∧ (𝜑𝜃))))
261, 25syl5bi 245 . . . 4 ((𝜑 → (𝜓𝜒)) → ((𝜃𝜒) → ((𝜒𝜃) ∧ (𝜑𝜃))))
27 nannan 1488 . . . 4 ((𝜑 ⊼ (𝜓𝜒)) ↔ (𝜑 → (𝜓𝜒)))
28 nannan 1488 . . . 4 (((𝜃𝜒) ⊼ ((𝜒𝜃) ⊼ (𝜑𝜃))) ↔ ((𝜃𝜒) → ((𝜒𝜃) ∧ (𝜑𝜃))))
2926, 27, 283imtr4i 295 . . 3 ((𝜑 ⊼ (𝜓𝜒)) → ((𝜃𝜒) ⊼ ((𝜒𝜃) ⊼ (𝜑𝜃))))
3029ancli 552 . 2 ((𝜑 ⊼ (𝜓𝜒)) → ((𝜑 ⊼ (𝜓𝜒)) ∧ ((𝜃𝜒) ⊼ ((𝜒𝜃) ⊼ (𝜑𝜃)))))
31 nannan 1488 . 2 (((𝜑 ⊼ (𝜓𝜒)) ⊼ ((𝜑 ⊼ (𝜓𝜒)) ⊼ ((𝜃𝜒) ⊼ ((𝜒𝜃) ⊼ (𝜑𝜃))))) ↔ ((𝜑 ⊼ (𝜓𝜒)) → ((𝜑 ⊼ (𝜓𝜒)) ∧ ((𝜃𝜒) ⊼ ((𝜒𝜃) ⊼ (𝜑𝜃))))))
3230, 31mpbir 234 1 ((𝜑 ⊼ (𝜓𝜒)) ⊼ ((𝜑 ⊼ (𝜓𝜒)) ⊼ ((𝜃𝜒) ⊼ ((𝜒𝜃) ⊼ (𝜑𝜃)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  wo 844  wnan 1482
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-nan 1483
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator