let p, q, r be Element of MC-wff ; :: thesis: ( {p} |-_IPC r & {q} |-_IPC r implies {(p 'or' q)} |-_IPC r )
set U = p 'or' q;
set X = {(p 'or' q)};
A2: |-_IPC (p => r) => ((q => r) => ((p 'or' q) => r)) by Th35;
assume A1: ( {p} |-_IPC r & {q} |-_IPC r ) ; :: thesis: {(p 'or' q)} |-_IPC r
then A5: |-_IPC q => r by Th54;
|-_IPC p => r by A1, Th54;
then |-_IPC (q => r) => ((p 'or' q) => r) by A2, Th37;
then A7: |-_IPC (p 'or' q) => r by A5, Th37;
{} c= {(p 'or' q)} ;
then {(p 'or' q)} |-_IPC (p 'or' q) => r by A7, Th66;
hence {(p 'or' q)} |-_IPC r by Th27, Th65; :: thesis: verum