( P <--> Q ) <--> (P->Q) and (Q->P)
<--> (~P V Q) and (~Q V P)
<--> (~P and (~Q V P)) V ( Q and (~Q V P))
<--> ((~P and ~Q) V (~P and P)) V ((Q and ~Q) V (Q and P))
<--> ((~P and ~Q) V False) V (False V (Q and P))
<--> (~P and ~Q) V (Q and P)
==> (~P and ~Q) V (Q and P)