let p, q, r be Element of MC-wff ; :: thesis: |-_IPC ((p => r) '&' (q => r)) => ((p 'or' q) => r)
set X = {((p => r) '&' (q => r))};
A1: {((p => r) '&' (q => r))} |-_IPC p => r by Th73;
A2: {((p => r) '&' (q => r))} |-_IPC q => r by Th74;
{((p => r) '&' (q => r))} |-_IPC (p => r) => ((q => r) => ((p 'or' q) => r)) by Th25;
then {((p => r) '&' (q => r))} |-_IPC (q => r) => ((p 'or' q) => r) by A1, Th27;
then {((p => r) '&' (q => r))} |-_IPC (p 'or' q) => r by A2, Th27;
hence |-_IPC ((p => r) '&' (q => r)) => ((p 'or' q) => r) by Th54; :: thesis: verum