theorem :: INTPRO_2:148

for p, q being Element of MC-wff holds |-_IPC (neg (p 'or' q)) 'equiv' ((neg p) '&' (neg q)) by Th99;