Theorem 1.4.12 (Completeness of the Heyting semantics). A proposition is provable in IPC if and only if it is $H$-valid for every Heyting algebra $H$.