let p, q, r be Element of MC-wff ; :: thesis: (r => p) => ((r => q) => (r => (p '&' q))) in IPC-Taut
A1: (r => (q => (p '&' q))) => ((r => q) => (r => (p '&' q))) in IPC-Taut by Def14;
p => (q => (p '&' q)) in IPC-Taut by Def14;
then A2: r => (p => (q => (p '&' q))) in IPC-Taut by Th18;
(r => (p => (q => (p '&' q)))) => ((r => p) => (r => (q => (p '&' q)))) in IPC-Taut by Def14;
then (r => p) => (r => (q => (p '&' q))) in IPC-Taut by A2, Def14;
hence (r => p) => ((r => q) => (r => (p '&' q))) in IPC-Taut by A1, Th26; :: thesis: verum