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 33662
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 1476 . . . . 5 ((𝜃𝜒) ↔ ¬ (𝜃𝜒))
2 pm4.57 984 . . . . . . . 8 (¬ (¬ (𝜒𝜃) ∧ ¬ (𝜑𝜃)) ↔ ((𝜒𝜃) ∨ (𝜑𝜃)))
3 orel2 884 . . . . . . . . . . . . 13 𝜑 → ((𝜒𝜑) → 𝜒))
43com12 32 . . . . . . . . . . . 12 ((𝜒𝜑) → (¬ 𝜑𝜒))
5 simpr 485 . . . . . . . . . . . . 13 ((𝜓𝜒) → 𝜒)
65a1i 11 . . . . . . . . . . . 12 ((𝜒𝜑) → ((𝜓𝜒) → 𝜒))
74, 6jad 188 . . . . . . . . . . 11 ((𝜒𝜑) → ((𝜑 → (𝜓𝜒)) → 𝜒))
87com12 32 . . . . . . . . . 10 ((𝜑 → (𝜓𝜒)) → ((𝜒𝜑) → 𝜒))
9 pm3.45 621 . . . . . . . . . . . 12 ((𝜒𝜒) → ((𝜒𝜃) → (𝜒𝜃)))
10 pm3.45 621 . . . . . . . . . . . 12 ((𝜑𝜒) → ((𝜑𝜃) → (𝜒𝜃)))
119, 10anim12i 612 . . . . . . . . . . 11 (((𝜒𝜒) ∧ (𝜑𝜒)) → (((𝜒𝜃) → (𝜒𝜃)) ∧ ((𝜑𝜃) → (𝜒𝜃))))
12 jaob 955 . . . . . . . . . . 11 (((𝜒𝜑) → 𝜒) ↔ ((𝜒𝜒) ∧ (𝜑𝜒)))
13 jaob 955 . . . . . . . . . . 11 ((((𝜒𝜃) ∨ (𝜑𝜃)) → (𝜒𝜃)) ↔ (((𝜒𝜃) → (𝜒𝜃)) ∧ ((𝜑𝜃) → (𝜒𝜃))))
1411, 12, 133imtr4i 293 . . . . . . . . . 10 (((𝜒𝜑) → 𝜒) → (((𝜒𝜃) ∨ (𝜑𝜃)) → (𝜒𝜃)))
158, 14syl 17 . . . . . . . . 9 ((𝜑 → (𝜓𝜒)) → (((𝜒𝜃) ∨ (𝜑𝜃)) → (𝜒𝜃)))
16 pm3.22 460 . . . . . . . . 9 ((𝜒𝜃) → (𝜃𝜒))
1715, 16syl6 35 . . . . . . . 8 ((𝜑 → (𝜓𝜒)) → (((𝜒𝜃) ∨ (𝜑𝜃)) → (𝜃𝜒)))
182, 17syl5bi 243 . . . . . . 7 ((𝜑 → (𝜓𝜒)) → (¬ (¬ (𝜒𝜃) ∧ ¬ (𝜑𝜃)) → (𝜃𝜒)))
1918con1d 147 . . . . . 6 ((𝜑 → (𝜓𝜒)) → (¬ (𝜃𝜒) → (¬ (𝜒𝜃) ∧ ¬ (𝜑𝜃))))
20 df-nan 1476 . . . . . . . 8 ((𝜒𝜃) ↔ ¬ (𝜒𝜃))
2120biimpri 229 . . . . . . 7 (¬ (𝜒𝜃) → (𝜒𝜃))
22 df-nan 1476 . . . . . . . 8 ((𝜑𝜃) ↔ ¬ (𝜑𝜃))
2322biimpri 229 . . . . . . 7 (¬ (𝜑𝜃) → (𝜑𝜃))
2421, 23anim12i 612 . . . . . 6 ((¬ (𝜒𝜃) ∧ ¬ (𝜑𝜃)) → ((𝜒𝜃) ∧ (𝜑𝜃)))
2519, 24syl6 35 . . . . 5 ((𝜑 → (𝜓𝜒)) → (¬ (𝜃𝜒) → ((𝜒𝜃) ∧ (𝜑𝜃))))
261, 25syl5bi 243 . . . 4 ((𝜑 → (𝜓𝜒)) → ((𝜃𝜒) → ((𝜒𝜃) ∧ (𝜑𝜃))))
27 nannan 1481 . . . 4 ((𝜑 ⊼ (𝜓𝜒)) ↔ (𝜑 → (𝜓𝜒)))
28 nannan 1481 . . . 4 (((𝜃𝜒) ⊼ ((𝜒𝜃) ⊼ (𝜑𝜃))) ↔ ((𝜃𝜒) → ((𝜒𝜃) ∧ (𝜑𝜃))))
2926, 27, 283imtr4i 293 . . 3 ((𝜑 ⊼ (𝜓𝜒)) → ((𝜃𝜒) ⊼ ((𝜒𝜃) ⊼ (𝜑𝜃))))
3029ancli 549 . 2 ((𝜑 ⊼ (𝜓𝜒)) → ((𝜑 ⊼ (𝜓𝜒)) ∧ ((𝜃𝜒) ⊼ ((𝜒𝜃) ⊼ (𝜑𝜃)))))
31 nannan 1481 . 2 (((𝜑 ⊼ (𝜓𝜒)) ⊼ ((𝜑 ⊼ (𝜓𝜒)) ⊼ ((𝜃𝜒) ⊼ ((𝜒𝜃) ⊼ (𝜑𝜃))))) ↔ ((𝜑 ⊼ (𝜓𝜒)) → ((𝜑 ⊼ (𝜓𝜒)) ∧ ((𝜃𝜒) ⊼ ((𝜒𝜃) ⊼ (𝜑𝜃))))))
3230, 31mpbir 232 1 ((𝜑 ⊼ (𝜓𝜒)) ⊼ ((𝜑 ⊼ (𝜓𝜒)) ⊼ ((𝜃𝜒) ⊼ ((𝜒𝜃) ⊼ (𝜑𝜃)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 841  wnan 1475
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 208  df-an 397  df-or 842  df-nan 1476
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator