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