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