Theorem: impliesAndImplies (NazgandLean4/Prop.lean)

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