let p, q, r be Element of CQC-WFF ; :: thesis: ( p => q in TAUT implies (r '&' p) => (r '&' q) in TAUT )
A1: ('not' (r => ('not' q))) => (r '&' q) in TAUT by Th16;
assume p => q in TAUT ; :: thesis: (r '&' p) => (r '&' q) in TAUT
then ('not' q) => ('not' p) in TAUT by LUKASI_1:34;
then A2: r => (('not' q) => ('not' p)) in TAUT by LUKASI_1:13;
(r => (('not' q) => ('not' p))) => ((r => ('not' q)) => (r => ('not' p))) in TAUT by LUKASI_1:11;
then (r => ('not' q)) => (r => ('not' p)) in TAUT by A2, CQC_THE1:46;
then A3: ('not' (r => ('not' p))) => ('not' (r => ('not' q))) in TAUT by LUKASI_1:34;
(r '&' p) => ('not' (r => ('not' p))) in TAUT by Th15;
then (r '&' p) => ('not' (r => ('not' q))) in TAUT by A3, LUKASI_1:3;
hence (r '&' p) => (r '&' q) in TAUT by A1, LUKASI_1:3; :: thesis: verum