let p, q, s be Element of MC-wff ; :: thesis: ((p '&' q) '&' s) => (p '&' s) in IPC-Taut
set P = p '&' q;
A1: (p '&' q) => p in IPC-Taut by Def14;
((p '&' q) => p) => (((p '&' q) '&' s) => (p '&' s)) in IPC-Taut by Th44;
hence ((p '&' q) '&' s) => (p '&' s) in IPC-Taut by A1, Def14; :: thesis: verum