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)) '&' (All (x,q))) is valid & ((All (x,p)) '&' (All (x,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)) '&' (All (x,q))) is valid & ((All (x,p)) '&' (All (x,q))) => (All (x,(p '&' q))) is valid )
let x be bound_QC-variable of A; :: thesis: ( (All (x,(p '&' q))) => ((All (x,p)) '&' (All (x,q))) is valid & ((All (x,p)) '&' (All (x,q))) => (All (x,(p '&' q))) is valid )
( (All (x,p)) => p is valid & (All (x,q)) => q is valid ) by CQC_THE1:66;
then A1: ((All (x,p)) '&' (All (x,q))) => (p '&' q) is valid by Lm5;
( All (x,((p '&' q) => q)) is valid & (All (x,((p '&' q) => q))) => ((All (x,(p '&' q))) => (All (x,q))) is valid ) by Lm1, Th23, Th30;
then A2: (All (x,(p '&' q))) => (All (x,q)) is valid by CQC_THE1:65;
( All (x,((p '&' q) => p)) is valid & (All (x,((p '&' q) => p))) => ((All (x,(p '&' q))) => (All (x,p))) is valid ) by Lm1, Th23, Th30;
then (All (x,(p '&' q))) => (All (x,p)) is valid by CQC_THE1:65;
hence (All (x,(p '&' q))) => ((All (x,p)) '&' (All (x,q))) is valid by A2, Lm3; :: thesis: ((All (x,p)) '&' (All (x,q))) => (All (x,(p '&' q))) is valid
( not x in still_not-bound_in (All (x,p)) & not x in still_not-bound_in (All (x,q)) ) by Th5;
then not x in still_not-bound_in ((All (x,p)) '&' (All (x,q))) by Th8;
hence ((All (x,p)) '&' (All (x,q))) => (All (x,(p '&' q))) is valid by A1, CQC_THE1:67; :: thesis: verum