theorem Th4: :: INTPRO_1:4

for X being Subset of MC-wff
for p, q being Element of MC-wff holds (p '&' q) => q in CnIPC X