theorem Th119: :: INTPRO_2:118

for X being Subset of MC-wff
for p, q, r being Element of MC-wff st X |-_IPC p & X \/ {r} |-_IPC q holds
X \/ {(p => r)} |-_IPC q