theorem :: INTPRO_2:161

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