let r, p, q be Element of CQC-WFF ; :: thesis: (r => p) => ((r => q) => (r => (p '&' q))) in TAUT
( r => (p => (q => (p '&' q))) in TAUT & (r => (p => (q => (p '&' q)))) => ((r => p) => (r => (q => (p '&' q)))) in TAUT ) by Th28, LUKASI_1:11, LUKASI_1:13;
then A1: (r => p) => (r => (q => (p '&' q))) in TAUT by CQC_THE1:46;
(r => (q => (p '&' q))) => ((r => q) => (r => (p '&' q))) in TAUT by LUKASI_1:11;
hence (r => p) => ((r => q) => (r => (p '&' q))) in TAUT by A1, LUKASI_1:3; :: thesis: verum