Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  const GIF version

Theorem const 837
 Description: Contraposition of a stable proposition. See comment of condc 838. (Contributed by BJ, 18-Nov-2023.)
Assertion
Ref Expression
const (STAB 𝜑 → ((¬ 𝜑 → ¬ 𝜓) → (𝜓𝜑)))

Proof of Theorem const
StepHypRef Expression
1 df-stab 816 . 2 (STAB 𝜑 ↔ (¬ ¬ 𝜑𝜑))
2 con3 631 . . 3 ((¬ 𝜑 → ¬ 𝜓) → (¬ ¬ 𝜓 → ¬ ¬ 𝜑))
3 notnot 618 . . . 4 (𝜓 → ¬ ¬ 𝜓)
4 imim2 55 . . . 4 ((¬ ¬ 𝜑𝜑) → ((¬ ¬ 𝜓 → ¬ ¬ 𝜑) → (¬ ¬ 𝜓𝜑)))
53, 4syl7 69 . . 3 ((¬ ¬ 𝜑𝜑) → ((¬ ¬ 𝜓 → ¬ ¬ 𝜑) → (𝜓𝜑)))
62, 5syl5 32 . 2 ((¬ ¬ 𝜑𝜑) → ((¬ 𝜑 → ¬ 𝜓) → (𝜓𝜑)))
71, 6sylbi 120 1 (STAB 𝜑 → ((¬ 𝜑 → ¬ 𝜓) → (𝜓𝜑)))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4  STAB wstab 815 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-in1 603  ax-in2 604 This theorem depends on definitions:  df-bi 116  df-stab 816 This theorem is referenced by:  condc  838
 Copyright terms: Public domain W3C validator