let p be Element of MC-wff ; :: thesis: |-_IPC p => p
A1: |-_IPC p => (p => p) by Th28;
A2: |-_IPC p => ((p => p) => p) by Th28;
|-_IPC (p => ((p => p) => p)) => ((p => (p => p)) => (p => p)) by Th29;
then |-_IPC (p => (p => p)) => (p => p) by A2, Th27;
hence |-_IPC p => p by A1, Th27; :: thesis: verum