Kind of a weird question. If propositions $P$ and $Q$ are equivalent and if we can show that, for some other proposition $R$, $P \implies R$ without using $Q$, then is there a proof of $Q \implies R$ that doesn't use $P$?
My thought is that if every proof of $Q \implies R$ ends up using $P$, then maybe $P$ and $Q$ are not equivalent after all.
Context: Part III here: Finding an almost complex structure (aka anti-involution) given an involution