Iff from `a → b` and `¬a → ¬b`

Stream: Is there code for X?

[Daniel Weber]

Do we have

example {a b : Prop} (h₁ : a → b) (h₂ : ¬a → ¬b) : a ↔ b := ⟨h₁, h₂.mtr⟩

somewhere? I was unable to locate it

[Kim Morrison]

Probably not.