let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (Ex (x,(p '&' q))) => ((Ex (x,p)) '&' (Ex (x,q))) is valid
let p, q be Element of CQC-WFF A; :: thesis: for x being bound_QC-variable of A holds (Ex (x,(p '&' q))) => ((Ex (x,p)) '&' (Ex (x,q))) is valid
let x be bound_QC-variable of A; :: thesis: (Ex (x,(p '&' q))) => ((Ex (x,p)) '&' (Ex (x,q))) is valid
All (x,((p '&' q) => q)) is valid by Lm1, Th23;
then A1: (Ex (x,(p '&' q))) => (Ex (x,q)) is valid by Th35;
All (x,((p '&' q) => p)) is valid by Lm1, Th23;
then (Ex (x,(p '&' q))) => (Ex (x,p)) is valid by Th35;
hence (Ex (x,(p '&' q))) => ((Ex (x,p)) '&' (Ex (x,q))) is valid by A1, Lm3; :: thesis: verum