theorem Th20: :: INTPRO_2:19

for X being Subset of MC-wff
for p, q being Element of MC-wff holds X |-_IPC (p '&' q) => p by INTPRO_1:3;