Biconditional introduction
The biconditional means if is the case, must be the case and if is the case, must be the case. Thus to introduce this operator we must demonstrate both that follows from and that follows from . We do this via two sub-proofs.
