case mpr =>
  intro hr
  cases hqr with
  | intro hqr_mp hqr_mpr =>
    cases hpq with
    | intro hpq_mp hpq_mpr =>
      apply hpq_mpr
      apply hqr_mpr
      exact hr
P Q R : Prop
hpq : P ↔ Q
hqr : Q ↔ R
⊢ R → P
no goals