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