¬φ ↔ φ → ⊥

φ¬φφ → ⊥¬φ ↔ (φ → ⊥)