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

(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