theorem :: INTPRO_2:37

for X being Subset of MC-wff
for p being Element of MC-wff st p is valid_IPC holds
X |-_IPC p