rw [biImpl_eq_impls]
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (biImpl φ₁ φ₂) ⊆ semVars φ₁ ∪ semVars φ₂
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars ((φ₁ ⇨ φ₂) ⊓ (φ₂ ⇨ φ₁)) ⊆ semVars φ₁ ∪ semVars φ₂