Theorem 1.5.4 (Glivenko’s Theorem). Assuming that:

  • φ and ψ are propositions

Then ⊢CPCφ→ψ if and only if ⊢IPC¬⁡¬⁡φ→¬⁡¬⁡ψ.