Theorem: impliesImplies (NazgandLean4/Prop.lean)

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