Theorem: LO.LogicalConnective.HomClass.map_iff (Logic/Logic/LogicSymbol.lean)

State before:
F : Type u_1
α : outParam (Type u_2)
β : outParam (Type u_3)
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
inst✝¹ : FunLike F α β
inst✝ : HomClass F α β
f : F
a b : α
⊢ f (a ⟷ b) = f a ⟷ f b
Tactic:
simp[LogicalConnective.iff]
State after:
no goals