let p, q be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable st Ex x,(p '&' q) is valid holds
(Ex x,p) '&' (Ex x,q) is valid
let x be bound_QC-variable; :: thesis: ( Ex x,(p '&' q) is valid implies (Ex x,p) '&' (Ex x,q) is valid )
assume A1: Ex x,(p '&' q) is valid ; :: thesis: (Ex x,p) '&' (Ex x,q) is valid
(Ex x,(p '&' q)) => ((Ex x,p) '&' (Ex x,q)) is valid by Th47;
hence (Ex x,p) '&' (Ex x,q) is valid by A1, CQC_THE1:104; :: thesis: verum