 The rejection of LEM in intuitionistic logic also implies the rejection of classical reductio ad absurdum as a legitimate method of (mathematical) proof. Intuitionistically, ad absurdum one can only prove negative statements (via negation introduction \((\phi \to \bot) \to \neg \phi\)). This is because the principle of double negation (\(\neg \neg \phi \to \phi\)) does not hold in intuitionistic logic. If it did, LEM would follow by modus ponens from the intuitionistically provable \(\neg \neg (\phi \vee \neg \phi)\) (in general it holds that if \(\phi\) is classically provable, then \(\neg\neg \phi\) is intuitionistically provable).