theorem :: INTPRO_2:156

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