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