theorem Th39: :: INTPRO_2:38

for p, q being Element of MC-wff holds p => (q => p) is valid_IPC