Theorem: impliesReorder (NazgandLean4/Prop.lean)

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