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