theorem :: INTPRO_2:147

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