theorem Th75: :: INTPRO_2:74

for p, q being Element of MC-wff holds |-_IPC ((p => q) '&' (p => (q => FALSUM))) => (p => FALSUM)