theorem Th27: :: INTPRO_2:26
for X being Subset of MC-wff
for p, q being Element of MC-wff st X |-_IPC p & X |-_IPC p => q holds
X |-_IPC q by INTPRO_1:10;