Let α, p, q and r be given.

Assume H1 H2.

Let β be given.

Assume H3.

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

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

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

∎