# Intuitionistic logic

That's true; if the $\alpha$'s are atomic formulas, then you can do it. The same goes for the Law of the Excluded Middle, that may be justified using BHK in this case.