$\gamma=(\psi \implies \phi)$ is a tautology $\equiv \psi$ is a contradiction or $\phi$ is a tautology. 
Prove that:
If $\psi,\phi$ are formulas such that $\text{VAR$(\psi)$} \cap\text{VAR$(\phi)$}=\emptyset$.
Then $\gamma=(\psi \implies \phi)$ is a tautology $\equiv \psi$  is a contradiction or $\phi$ is a tautology.

Attempt:
Let $v: \text{FORM} \to \textbf 2$ be a valuation. As $\gamma$ is a tautology, we have $v(\gamma)=1\forall v$ valuation.
Also $v(\gamma)=max(1-v(\psi),v(\phi))=1$, this happens if and only if $\left(v(\psi)=0 \text{ or } v(\psi)=1\right) \forall v$ valuation.
It seems to me that to complete my proof I'd have to "distribute" the "$\forall v$ valuation" to those two propositions. Can this be done?
Also, if the answer to the above question is no, are there cases where you can distribute the forall? Why/why not?
 A: First let me restate the question: it's to show that 


*

*if $\phi$ and $\psi$ have no propositional variables in common, then $\phi\to \psi$ is a tautology iff either $\phi$ is a contradiction or $\psi$ is a tautology.


So suppose $\phi,\psi$ have no variables in common.  
Now in one direction, suppose that $\phi\to\psi$ is not a tautology.  Then, there's a valuation $v$ on which $\phi$ is true while $\psi$ is false; the right-hand side clearly fails.
Conversely, suppose that the right-hand side fails, so that there's a valuation $v_1$ on which $\phi$ is true, and a valuation $v_2$ on which $\psi$ is false. Since $\phi,\psi$ have no variables in common, therefore there's a valuation $v$ which agrees with $v_1$ on the variables of $\phi$, and which agrees with $v_2$ on the variables of $\psi$.  Thus $\phi$ must be true on $v$ while $\psi$ is false on $v$, so that $\phi\to\psi$ is false on $v$.  Thus, the failure of the right-hand side implies the failure of the left-hand side.
I think the last couple of your sentences are about working with biconditionals in proofs.  This can turn out to be nastier than it looks, even in relatively simple cases.  One reason is just that formulas
$\forall x(A\leftrightarrow B)$
and
$\forall x A\leftrightarrow \forall xB$
are not equivalent.  The first implies the second, but not conversely.  (They inherit this relationship from the conditionals they conjoin.)
Applied to the context of the question: you can push the quantifier over valuations down to independent generalizations of two sides of the biconditional, and then chain together a bunch of iffs, but you won't be able to pull it back out again at the end.
The upshot is that biconditionals are often proved more clearly by splitting them into two directions.
