let p, q, r be Element of HP-WFF ; (p => (q => r)) => ((p '&' q) => r) in HP_TAUT
A1:
((p '&' q) => q) => ((q => r) => ((p '&' q) => r)) in HP_TAUT
by Th21;
(p '&' q) => q in HP_TAUT
by Def10;
then
(q => r) => ((p '&' q) => r) in HP_TAUT
by A1, Def10;
then A2:
p => ((q => r) => ((p '&' q) => r)) in HP_TAUT
by Th15;
A3:
(p => ((p '&' q) => r)) => ((p '&' q) => (p => r)) in HP_TAUT
by Th26;
(p => ((q => r) => ((p '&' q) => r))) => ((p => (q => r)) => (p => ((p '&' q) => r))) in HP_TAUT
by Def10;
then
(p => (q => r)) => (p => ((p '&' q) => r)) in HP_TAUT
by A2, Def10;
then A4:
(p => (q => r)) => ((p '&' q) => (p => r)) in HP_TAUT
by A3, Th23;
A5:
(p '&' q) => p in HP_TAUT
by Def10;
((p '&' q) => (p => r)) => (((p '&' q) => p) => ((p '&' q) => r)) in HP_TAUT
by Def10;
then
((p '&' q) => (p => r)) => ((p '&' q) => r) in HP_TAUT
by A5, Th29;
hence
(p => (q => r)) => ((p '&' q) => r) in HP_TAUT
by A4, Th23; verum