simp [← h₁, ← h₂, eval, biImpl]
ν : Type u_1
τ : PropAssignment ν
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ (eval τ (biImpl φ₁✝ φ₂✝) = true) = (eval τ φ₁✝ = eval τ φ₂✝)
no goals