let p, q, r be Element of HP-WFF ; :: thesis: ( p => (q => r) in HP_TAUT implies q => (p => r) in HP_TAUT )
assume A1: p => (q => r) in HP_TAUT ; :: thesis: q => (p => r) in HP_TAUT
A2: ((p => q) => (p => r)) => ((q => (p => q)) => (q => (p => r))) in HP_TAUT by Th19;
(p => (q => r)) => ((p => q) => (p => r)) in HP_TAUT by Def10;
then (p => q) => (p => r) in HP_TAUT by A1, Def10;
then A3: (q => (p => q)) => (q => (p => r)) in HP_TAUT by A2, Def10;
q => (p => q) in HP_TAUT by Def10;
hence q => (p => r) in HP_TAUT by A3, Def10; :: thesis: verum