Theorem: impliesIff (NazgandLean4/Prop.lean)

State before:
p q r : Prop
⊢ p → (q ↔ r) ↔ (p → q ↔ p → r)
Tactic:
tauto
State after:
no goals