Let alpha, p, q and r be given.

Assume H1 H2.

Let beta be given.

Assume H3.

Apply iff_trans (p beta) (q beta) to the current goal.

An exact proof term for the current goal is H1 beta H3.

An exact proof term for the current goal is H2 beta H3.

∎