I would not step to the esoteric or psychological level here. Let me introduce an easy example of two obviously equivalent statements: $\forall x Rx$ holds if and only if $(\exists x Px \lor \forall x\neg Px)\rightarrow \forall x Rx$, so
$$\forall x Rx \leftrightarrow((\exists x Px \lor \forall x\neg Px)\rightarrow \forall x Rx)$$
is a tautology. But see what happens if we prove the two directions in a sequent calculus:
The essence of the example: Just because two formulas $\varphi$ and $\psi$ are equivalent, this does not mean that the proofs of the logical true, but otherwise potentially substantially different formulas $\varphi\rightarrow\psi$ and $\psi\rightarrow\varphi$ are equally hard. In the example, we had to actually proof the premise $\exists x Px \lor \forall x\neg Px$ in the "$\leftarrow$" direction, while we could treat it in the "$\rightarrow$" direction as a blackbox.
Also: The logical equivalence of two formulas tells us nothing about the complexity of their respective proofs! This is no human psychology, just technical issues. And a genius would probably look at the formulas and state: "hey, but the second one will have a more complex proof" ;)
Remark: I you are not comfortable with the sequent calculus, regard it the following way: In the left-to-right direction, you can exploit the fact that $\varphi\rightarrow(\psi\rightarrow\varphi)$ is always true (propositional tautology), regardless of the truth of $\psi$. For $(\psi\rightarrow\varphi)\rightarrow\varphi$, you have to prove $\psi$ first, because only then this becomes logically true. All this is not effected by the fact that the formulas of the above example are equivalent, and both directions are therefore provable. Provability and complexity of proofs are two different things.
Edit: Now specifically addressing your questions -
- Is this actually an interesting phenomenon?
I'd vote for yes - but rather from the proof-theoretic "technical" point of view than from a philosophical one.
- If it is, is there any way to state it less "softly?"
Well, you could phrase it towards an investigation of the lengths of the shortest proofs (in a formal system) for the two directions of a bi-implication.
- Do you have any favorite examples of these theorems?
One of my favorites is the soundness and completeness of a formal proof system for first-order logic: A theorem is logically true if and only if it is provable in the system.
- Why is one direction easier in these cases?
The "$\leftarrow$" direction (soundness) is the easy one, you just have to do a structural induction over the calculus. The "$\rightarrow$" direction ((strong) completeness) is the complicated (and more interesting) one; interesting facts like the compactness theorem follow from the existence of such complete proof systems.