Do polynomial reduction functions work both ways?
The statement 


  Formula $F$ is satisfiable $\iff$ graph has an independent set


is imprecise, since it does not specify which graph we are taling about. Correcting this, we get:


  There is a polynomial-time function $\mathcal{G}$ from formulas to graphs such that, for all formulas $F$, $F$ is satisfiable $\iff$ $\mathcal{G}(F)$ has an independent set


Note that, once properly written like this, the statement is no longer symmetric: the reduction function goes in one way (formulas to graphs), and not the other way around. So, proving the above does not also prove the converse reduction.

The converse reduction (from independent set to 3-SAT) holds, but to prove that we need another reduction function $\mathcal{F}(G)$ mapping graphs into formulas.