Theorem: impliesAnd (NazgandLean4/Prop.lean)

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