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