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