Here is the deduction theorem, in the "$\Leftrightarrow$" version (I'm considering it for first order logic): $$\Delta \cup \lbrace A \rbrace \vdash \lbrace B \rbrace \Longleftrightarrow \Delta \vdash \lbrace A \rightarrow B \rbrace$$ where $\Delta$, $\lbrace A \rbrace$ and so on are sets of formulas. I'm taking set theory (ZFC, ZF or whatever) as the metatheory.
This metatheorem states that if we can prove $B$ assuming $\Delta$ and $A$, than we can prove $A \rightarrow B$ assuming only $\Delta$ and viceversa. With this metatheorem, if we want to prove a theorem in the form $A \rightarrow B$ we don't need to directly prove the implication, we just have to assume the formulas in $\Delta \cup \lbrace A \rbrace$ and derive $B$: that will be equivalent to prove $A \rightarrow B$ from $\Delta$.
This metatheorem is used in the everyday mathematics. In fact in most cases, when we want to prove an implication in the form $A \rightarrow B$ we always say "Assume $A$," and then with a chain of inferences we conclude $B$, and that is by the deduction theorem a proof of $A \rightarrow B.$
Now here is the question: in our metatheory (in this case it's set theory), we have proved an implication "$\Longrightarrow$" (precisely a double implication $\Longleftrightarrow$); the proofs of the deduction theorem that I've seen start always assuming "suppose $\Delta \cup \lbrace A \rbrace \vdash \lbrace B \rbrace$" and then they finish saying "...then $\Delta \vdash \lbrace A \rightarrow B \rbrace$" and so (doing that even in the other direction), we prove a metatheorem in the form $\psi \Longleftrightarrow \phi$... but aren't we implicitly assuming the deduction theorem "for our metatheory", since we proved an implication $ \psi \Longrightarrow \phi$, assuming $\Delta \cup \lbrace A \rbrace \vdash \lbrace B \rbrace$ and then deriving $\Delta \vdash \lbrace A \rightarrow B \rbrace$?
Is this observation correct or am I wrong? From what I know I guess that since in mathematics we can't start formalizing notions from no bases and we just have to assume something in our metatheory, in a certain sense we have to "assume" the deduction theorem in our metatheory to prove it for the object theory, but I'm not sure.
Tell me what you think and thanks in advance :D