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