Why do axiomatic systems for propositional calculus include IFF axioms? I am reading : https://en.wikipedia.org/wiki/Propositional_calculus#Axioms, and the following three axioms seemed unnecessary to me:
$$
 IFF-1 : ( \phi \iff \chi ) \implies (\phi \implies \chi ) \\
 IFF-2 : ( \phi \iff \chi ) \implies (\chi \implies \phi ) \\
 IFF-3 : ( \phi \implies \chi ) \implies ( ( \chi \implies \phi ) \implies ( \phi \iff \chi ) )
$$
I understand how they would define an $ \iff $ operator, but wouldn't you always be able to substitute $(\phi \implies \chi) \land (\chi \implies \phi)$ for $ (\phi \iff \chi) $ in any proof? From $(\phi \implies \chi) \land (\chi \implies \phi)$ and the three $\land$ axioms you can recover the three $\iff$ axioms. In this scheme $ (\phi \iff \chi) $ in proofs would be notation for ($\phi \implies \chi) \land (\chi \implies \phi)$.
You would end up with an equivalent notion with three fewer axioms and one fewer operator in the system.

"I understand how they would define an ⟺ operator, but wouldn't you always be able to substitute (ϕ⟹χ)∧(χ⟹ϕ) for (ϕ⟺χ) in any proof?"
No.  In intuitionistic logic, such substitution is not necessarily allowed, since defining (ϕ⟺χ) in terms of $\land$ and ⟹ is not possible necessarily.  Definiability of distinct connectives is not allowed in at least some intuitionistic logical systems.
Also, using definable connectives is sometimes disallowed in proofs.  Definition-free proofs would disallow using ((ϕ⟹χ)∧(χ⟹ϕ)) for (ϕ⟺χ) in any proof.
