Theorem: LO.Semantics.realize_iff (Logic/Logic/Semantics.lean)

State before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Tarski M
𝓜 : M
p q : F
⊢ 𝓜 ⊧ p ⟷ q ↔ (𝓜 ⊧ p ↔ 𝓜 ⊧ q)
Tactic:
simp [LogicalConnective.iff, iff_iff_implies_and_implies]
State after:
no goals