Theorem: LO.LogicalConnective.Prop.iff_eq (Logic/Logic/LogicSymbol.lean)

State before:
p q : Prop
⊢ p ⟷ q = (p ↔ q)
Tactic:
simp[LogicalConnective.iff, iff_iff_implies_and_implies]
State after:
no goals