let p, q be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable holds (All (x,(p '&' q))) => ((All (x,p)) '&' q) is valid
let x be bound_QC-variable; :: thesis: (All (x,(p '&' q))) => ((All (x,p)) '&' q) is valid
A1: (q '&' (All (x,p))) => ((All (x,p)) '&' q) is valid by CQC_THE1:64;
( All (x,((p '&' q) => (q '&' p))) is valid & (All (x,((p '&' q) => (q '&' p)))) => ((All (x,(p '&' q))) => (All (x,(q '&' p)))) is valid ) by Th26, Th34, CQC_THE1:64;
then A2: (All (x,(p '&' q))) => (All (x,(q '&' p))) is valid by CQC_THE1:65;
(All (x,(q '&' p))) => (q '&' (All (x,p))) is valid by Th68;
then (All (x,(p '&' q))) => (q '&' (All (x,p))) is valid by A2, LUKASI_1:42;
hence (All (x,(p '&' q))) => ((All (x,p)) '&' q) is valid by A1, LUKASI_1:42; :: thesis: verum