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