theorem :: INTPRO_2:130

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