Is this first-order proof valid? $(\forall x Qx \rightarrow P)\leftrightarrow\exists x (Qx \rightarrow P)$

Question

Is my theorem wrong? If so where did I mess up?

The following first-order theorem doesn't feel right to me.

$$(\forall x Qx \rightarrow P)\leftrightarrow\exists x (Qx \rightarrow P)$$

(Where $x$ is not free in $P$)

Particularly:

$\exists x (Qx \rightarrow P)\rightarrow(\forall x Qx \rightarrow P)$

I am trying to prove first-order identities to be able to make more effective proofs in the future for my personal study.

I produced the following theorems using rules of inference.

I also used two theorems, which I mention after the main proof.

Theorem 1.1

1. $\forall x Qx \rightarrow P$
   premise
2. $\neg \forall x Qx \lor P$
   material implication (1)
3. $\exists x \neg Qx \lor P$
   theorem A (2)
4. $\exists x (\neg Qx \lor P)$
   theorem B (3)
5. $\exists x (Qx \rightarrow P)$ material implication (4)
6. $(\forall x Qx \rightarrow P)\rightarrow\exists x (Qx \rightarrow P)$
   deduction theorem (1)(5)

Theorem 1.2

1. $\exists x (Qx \rightarrow P)$
   premise
2. $\exists x (\neg Qx \lor P)$
   material implication (1)
3. $\exists x \neg Qx \lor P$
   theorem B (2)
4. $\neg \forall x Qx \lor P$
   theorem A (3)
5. $\forall x Qx \rightarrow P$
   material implication (4)
6. $\exists x (Qx \rightarrow P)\rightarrow(\forall x Qx \rightarrow P)$
   deduction theorem (1)(5)

Theorem 1.3

1. $(\forall x Qx \rightarrow P)\rightarrow\exists x (Qx \rightarrow P)$
   theorem 1.1
2. $\exists x (Qx \rightarrow P)\rightarrow(\forall x Qx \rightarrow P)$
   theorem 1.2
3. $(\forall x Qx \rightarrow P)\leftrightarrow\exists x (Qx \rightarrow P)$
   biconditional introduction (1)(2)

Theorems A and B are mentioned below for reference:

Theorem A: $$\neg\forall xPx\leftrightarrow \exists x\neg Px$$

Theorem B $$P\lor\exists xQx\leftrightarrow \exists x (P \lor Qx)$$

I will only show my proof of theorem B, but if requested I will show my proof of theorem A.

Theorem B.1

1. $P \lor \exists x Qx$
   premise
2. $\exists x Qx$
   premise
3. $Qx$
   existential instantiation (2)
4. $P\lor Qx$
   addition (right) (3)
5. $\exists x (P \lor Qx)$
   existential generalization (4)
6. $\exists x Qx \rightarrow \exists x (P \lor Qx)$
   deduction theorem (2)(5)
7. $P$
   premise
8. $P \lor Qx$
   addition (left) (7)
9. $\exists x (P \lor Qx)$
   existential generalization (8)
10. $P \rightarrow \exists x (P \lor Qx)$
    deduction theorem (7)(9)
11. $\exists x (P \lor Qx)\lor\exists x (P \lor Qx)$
    constructive dilemma (10)(6)(1)
12. $\exists x (P \lor Qx)$
    idempotency of disjunction (11)
13. $P\lor\exists xQx\rightarrow \exists x (P \lor Qx)$
    deduction theorem (1)(12)

Theorem B.2

1. $\exists x (P \lor Qx)$
   premise
2. $P \lor Qx$ existential instantiation
3. $P$
   premise
4. $P \lor \exists x Qx$
   addition (left)
5. $P \rightarrow P \lor \exists x Qx$
   deduction theorem (3)(4)
6. $Qx$
   premise
7. $\exists x Qx$
   existential generalization
8. $P \lor \exists x Qx$
   addition (right)
9. $Qx \rightarrow P \lor \exists x Qx$
   deduction theorem (6)(9)
10. $(P\lor \exists xQx)\lor(P\lor \exists xQx)$
    constructive dilemma (5)(9)(2)
11. $P\lor \exists xQx$
    idempotency of disjunction (10)
12. $\exists x (P \lor Qx) \rightarrow P \lor \exists x Qx$
    deduction theorem (1)(12)

Theorem B

1. $P\lor\exists xQx\rightarrow \exists x (P \lor Qx)$
   theorem B.1
2. $\exists x (P \lor Qx) \rightarrow P \lor \exists x Qx$ theorem B.2
3. $P\lor\exists xQx\leftrightarrow \exists x (P \lor Qx)$ biconditional introduction (1)(2)