theorem Th31: :: INTPRO_2:30

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