theorem Th78: :: INTPRO_2:77

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