let p, q, s be Element of HP-WFF ; :: thesis: ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in HP_TAUT
A1: (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in HP_TAUT by Lm6;
((p '&' q) '&' s) => (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) in HP_TAUT by Th30;
hence ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in HP_TAUT by A1, Th23; :: thesis: verum