let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid & (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid )
let p, q be Element of CQC-WFF A; :: thesis: for x being bound_QC-variable of A st not x in still_not-bound_in p holds
( (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid & (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid )
let x be bound_QC-variable of A; :: thesis: ( not x in still_not-bound_in p implies ( (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid & (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid ) )
assume A1: not x in still_not-bound_in p ; :: thesis: ( (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid & (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid )
(p '&' q) => (Ex (x,(p '&' q))) is valid by Th15;
then A2: q => (p => (Ex (x,(p '&' q)))) is valid by Th4;
not x in still_not-bound_in (Ex (x,(p '&' q))) by Th6;
then not x in still_not-bound_in (p => (Ex (x,(p '&' q)))) by A1, Th7;
then (Ex (x,q)) => (p => (Ex (x,(p '&' q)))) is valid by A2, Th19;
hence (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid by Th2; :: thesis: (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid
q => (Ex (x,q)) is valid by Th15;
then A3: (p '&' q) => (p '&' (Ex (x,q))) is valid by Lm9;
not x in still_not-bound_in (Ex (x,q)) by Th6;
then not x in still_not-bound_in (p '&' (Ex (x,q))) by A1, Th8;
hence (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid by A3, Th19; :: thesis: verum