Intuitionistic (constructive) logic is similar to classical logic with the notable omission of ax-3 and theorems such as exmid or peirce. We mostly treat intuitionistic logic in a separate file, iset.mm, which is known as the Intuitionistic Logic Explorer on the web site. However, iset.mm has a number of additional axioms (mainly to replace definitions like df-or and df-ex which are not valid in intuitionistic logic) and we want to prove those axioms here to demonstrate that adding those axioms in iset.mm does not make iset.mm any less consistent than set.mm.
The following axioms are unchanged between set.mm and iset.mm: ax-1, ax-2, ax-mp, ax-4, ax-11, ax-gen, ax-7, ax-12, ax-8, ax-9, and ax-5.
In this list of axioms, the ones that repeat earlier theorems are marked "(New usage is discouraged.)" so that the earlier theorems will be used consistently in other proofs.