theorem :: INTPRO_2:116

for Y, X being Subset of MC-wff
for q, r being Element of MC-wff st X |-_IPC r & Y \/ {r} |-_IPC q holds
X \/ Y |-_IPC q