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

State before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Tarski M
𝓜 : M
s : Finset F
⊢ 𝓜 ⊧ ⋀s ↔ ∀ p ∈ s, 𝓜 ⊧ p
Tactic:
simp [Finset.conj]
State after:
no goals