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