apply subset_trans (semVars_conj _ _)
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars ((φ₁ ⇨ φ₂) ⊓ (φ₂ ⇨ φ₁)) ⊆ semVars φ₁ ∪ semVars φ₂
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₁ ⇨ φ₂) ∪ semVars (φ₂ ⇨ φ₁) ⊆ semVars φ₁ ∪ semVars φ₂