theorem Th53: :: INTPRO_2:52

for X being Subset of MC-wff
for F, G being Element of MC-wff st X \/ {F} |-_IPC G holds
X |-_IPC F => G