let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (All (x,(p '&' q))) => ((All (x,p)) '&' q) is valid
let p, q be Element of CQC-WFF A; :: thesis: for x being bound_QC-variable of A holds (All (x,(p '&' q))) => ((All (x,p)) '&' q) is valid
let x be bound_QC-variable of A; :: 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 Th23, Th30, 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 Th64;
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