Theorem: SetTheory.interpret_and (SetTheory/Formula.lean)

State before:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p q : BoundedFormula α✝ a✝
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.and p q) v l ↔ Interpret V p v l ∧ Interpret V q v l
Tactic:
rw [and_iff]
State after:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p q : BoundedFormula α✝ a✝
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.and p q) v l ↔ ¬(Interpret V p v l → ¬Interpret V q v l)

State before:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p q : BoundedFormula α✝ a✝
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.and p q) v l ↔ ¬(Interpret V p v l → ¬Interpret V q v l)
Tactic:
rfl
State after:
no goals