Let A and B be given.

Assume H1: (A → B) ∧ (B → A).

Apply H1 to the current goal.

Assume H2: A → B.

Assume H3: B → A.

An exact proof term for the current goal is iffI B A H3 H2.

∎