The 'necessity' part of PleftrightarrowQP \\leftrightarrow QPleftrightarrowQ refers to:
PrightarrowQP \\rightarrow QPrightarrowQ
QrightarrowPQ \\rightarrow PQrightarrowP
negQ\\neg QnegQ
PlorQP \\lor QPlorQ