Biconditional introduction

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