let X be Subset of MC-wff; :: thesis: 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
let p, q, r be Element of MC-wff ; :: thesis: ( X \/ {p} |-_IPC r & X \/ {q} |-_IPC r implies X \/ {(p 'or' q)} |-_IPC r )
set U = p 'or' q;
assume A1: ( X \/ {p} |-_IPC r & X \/ {q} |-_IPC r ) ; :: thesis: X \/ {(p 'or' q)} |-_IPC r
then A2: X |-_IPC p => r by Th53;
A3: X |-_IPC q => r by A1, Th53;
X |-_IPC (p => r) => ((q => r) => ((p 'or' q) => r)) by Th25;
then X |-_IPC (q => r) => ((p 'or' q) => r) by A2, Th27;
then A6: X |-_IPC (p 'or' q) => r by A3, Th27;
A7: {(p 'or' q)} |-_IPC p 'or' q by Th65;
{(p 'or' q)} c= X \/ {(p 'or' q)} by XBOOLE_1:7;
then A11: X \/ {(p 'or' q)} |-_IPC p 'or' q by A7, Th66;
X c= X \/ {(p 'or' q)} by XBOOLE_1:7;
then X \/ {(p 'or' q)} |-_IPC (p 'or' q) => r by A6, Th66;
hence X \/ {(p 'or' q)} |-_IPC r by A11, Th27; :: thesis: verum