let A be QC-alphabet ; 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
(Ex (x,(p => q))) => (p => (Ex (x,q))) is valid
let p, q be Element of CQC-WFF A; for x being bound_QC-variable of A st not x in still_not-bound_in p holds
(Ex (x,(p => q))) => (p => (Ex (x,q))) is valid
let x be bound_QC-variable of A; ( not x in still_not-bound_in p implies (Ex (x,(p => q))) => (p => (Ex (x,q))) is valid )
assume A1:
not x in still_not-bound_in p
; (Ex (x,(p => q))) => (p => (Ex (x,q))) is valid
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, Th7;
then A2:
(Ex (x,(p => (Ex (x,q))))) => (p => (Ex (x,q))) is valid
by Th20;
q => (Ex (x,q)) is valid
by Th15;
then A3:
All (x,((p => q) => (p => (Ex (x,q))))) is valid
by Th23, LUKASI_1:51;
(All (x,((p => q) => (p => (Ex (x,q)))))) => ((Ex (x,(p => q))) => (Ex (x,(p => (Ex (x,q)))))) is valid
by Th34;
then
(Ex (x,(p => q))) => (Ex (x,(p => (Ex (x,q))))) is valid
by A3, CQC_THE1:65;
hence
(Ex (x,(p => q))) => (p => (Ex (x,q))) is valid
by A2, LUKASI_1:42; verum