and_imp_right_iff

Stream: Is there code for X?

[Jireh Loreaux]

This seems to be missing? It's the ↔ version of docs#And.imp_right, and it seems like something that should have come up before. In fact, I would have expected this to be a simp lemma (or even we could have a simproc that doesn't require it to be on the same side).

lemma and_imp_right_iff {a b c : Prop} : (a ∧ b → a ∧ c) ↔ a → b → c := by
  tauto

[Aaron Liu]

Does simp +contextual solve this?

[Aaron Liu]

this wouldn't be a simp lemma since we have docs#and_imp

[Jireh Loreaux]

ah, indeed.