let p, q, s be Element of HP-WFF ; :: thesis: ((p '&' q) '&' s) => (p '&' s) in HP_TAUT
set P = p '&' q;
A1: (p '&' q) => p in HP_TAUT by Def10;
((p '&' q) => p) => (((p '&' q) '&' s) => (p '&' s)) in HP_TAUT by Th41;
hence ((p '&' q) '&' s) => (p '&' s) in HP_TAUT by A1, Def10; :: thesis: verum