c a b : Prop
inst✝ : Decidable c
h : ¬c → (a ↔ b)
⊢ ¬c → a ↔ ¬c → b
c a b : Prop
inst✝ : Decidable c
h : ¬c → (a ↔ b)
⊢ a ∨ c ↔ b ∨ c
rw [or_iff_not_imp_right, or_iff_not_imp_right]
no goals
c a b : Prop
inst✝ : Decidable c
h : ¬c → (a ↔ b)
⊢ ¬c → a ↔ ¬c → b
exact imp_congr_right h