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