theorem :: INTPRO_2:160

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