Theorem: and_iff (SetTheory/Formula.lean)

State before:
V : Type ?u.6701
inst✝ : SetTheory V
p q : Prop
⊢ p ∧ q ↔ ¬(p → ¬q)
Tactic:
by_cases p <;> aesop
State after:
no goals