theorem Th123: :: INTPRO_2:122

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