let p, q be Element of MC-wff ; :: thesis: {(p '&' q)} |-_IPC q
A1: {(p '&' q)} |-_IPC (p '&' q) => q by Th21;
{(p '&' q)} |-_IPC p '&' q by Th65;
hence {(p '&' q)} |-_IPC q by A1, Th27; :: thesis: verum