theorem Th39: :: INTPRO_1:39

for p, q being Element of MC-wff holds ((p => q) '&' p) => q in IPC-Taut