Zulip Chat Archive
Stream: Is there code for X?
Topic: iff imp distrib
Kyle Miller (Mar 23 2023 at 17:27):
Do we have this trivial lemma anywhere already?
example (p q r : Prop) : (p → (q ↔ r)) ↔ ((p → q) ↔ (p → r)) := by tauto
Pedro Sánchez Terraf (Mar 23 2023 at 18:58):
It follows from distributivity of disjunction, if you have that one
Yaël Dillies (Mar 23 2023 at 20:14):
We have docs#himp_bihimp but not himp_bihimp_distrib. :frowning:
Last updated: May 02 2025 at 03:31 UTC