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