theorem Th42: :: INTPRO_2:41

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