let r, p, q be Element of CQC-WFF ; :: thesis: ( r => p in TAUT & r => q in TAUT implies r => (p '&' q) in TAUT )
assume that
A1: r => p in TAUT and
A2: r => q in TAUT ; :: thesis: r => (p '&' q) in TAUT
(r => p) => ((r => q) => (r => (p '&' q))) in TAUT by Th33;
then (r => q) => (r => (p '&' q)) in TAUT by A1, CQC_THE1:82;
hence r => (p '&' q) in TAUT by A2, CQC_THE1:82; :: thesis: verum