The biconditional is a basic operation in propositional logic. The statment φ ↔ ψ means that φ is true if and only if ψ is true. It means that φ implies ψ and that ψ implies φ.
The biconditional is the first operation in Ghilbert to be defined. The conditional → and negation ¬ are included in the axioms, but the biconditional is not. The initial definition of the biconditional is quite complicated and difficult to follow. This is because the definition cannot use the biconditional or any operator other than → and ¬. From this definition, we can derive simpler expressions that define the bicondition (see dfbi1, dfbi3, and dfbi). Once conjunction is introduced this definition can be rewritten in a simple form as (<-> (<-> ph ps) (/\ (-> ph ps) (-> ps ph))) /edit/peano/prop.gh/dfbi2.