Let A, B and C be given.

Assume H1: A ↔ B.

Assume H2: B ↔ C.

Apply H1 to the current goal.

Assume H3: A → B.

Assume H4: B → A.

Apply H2 to the current goal.

Assume H5: B → C.

Assume H6: C → B.

An exact proof term for the current goal is (iffI A C (λH ⇒ H5 (H3 H)) (λH ⇒ H4 (H6 H))).

∎