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