Theorem: LO.FirstOrder.ModelsTheory.add_iff (Logic/FirstOrder/Basic/Semantics/Semantics.lean)

State before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type u_1
inst✝¹ : Nonempty M
inst✝ : Structure L M
T U : Theory L
⊢ M ⊧ₘ* T + U ↔ M ⊧ₘ* T ∧ M ⊧ₘ* U
Tactic:
simp [Theory.add_def]
State after:
no goals