let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A holds (p => (Ex (x,q))) => (Ex (x,(p => q))) is valid
let p, q be Element of CQC-WFF A; :: thesis: for x being bound_QC-variable of A holds (p => (Ex (x,q))) => (Ex (x,(p => q))) is valid
let x be bound_QC-variable of A; :: thesis: (p => (Ex (x,q))) => (Ex (x,(p => q))) is valid
( All (x,(('not' ('not' (p '&' ('not' q)))) => (p '&' ('not' q)))) is valid & (All (x,(('not' ('not' (p '&' ('not' q)))) => (p '&' ('not' q))))) => ((All (x,('not' ('not' (p '&' ('not' q)))))) => (All (x,(p '&' ('not' q))))) is valid ) by Th23, Th30;
then (All (x,('not' ('not' (p '&' ('not' q)))))) => (All (x,(p '&' ('not' q)))) is valid by CQC_THE1:65;
then A1: ('not' (All (x,(p '&' ('not' q))))) => ('not' (All (x,('not' ('not' (p '&' ('not' q))))))) is valid by LUKASI_1:52;
(All (x,('not' q))) <=> ('not' (Ex (x,q))) is valid by Th54;
then (All (x,('not' q))) => ('not' (Ex (x,q))) is valid by Lm14;
then (p '&' (All (x,('not' q)))) => (p '&' ('not' (Ex (x,q)))) is valid by Lm9;
then A2: ('not' (p '&' ('not' (Ex (x,q))))) => ('not' (p '&' (All (x,('not' q))))) is valid by LUKASI_1:52;
(All (x,(p '&' ('not' q)))) => (p '&' (All (x,('not' q)))) is valid by Th64;
then ('not' (p '&' (All (x,('not' q))))) => ('not' (All (x,(p '&' ('not' q))))) is valid by LUKASI_1:52;
then ('not' (p '&' ('not' (Ex (x,q))))) => ('not' (All (x,(p '&' ('not' q))))) is valid by A2, LUKASI_1:42;
then (p => (Ex (x,q))) => ('not' (All (x,(p '&' ('not' q))))) is valid by QC_LANG2:def 2;
then (p => (Ex (x,q))) => ('not' (All (x,('not' ('not' (p '&' ('not' q))))))) is valid by A1, LUKASI_1:42;
then (p => (Ex (x,q))) => ('not' (All (x,('not' (p => q))))) is valid by QC_LANG2:def 2;
hence (p => (Ex (x,q))) => (Ex (x,(p => q))) is valid by QC_LANG2:def 5; :: thesis: verum