simp only [eval_conj]
ν✝ : Type u_1
φ₁ φ₂ φ₃ : PropFun ν✝
h₁ : entails φ₁ φ₂
h₂ : entails φ₁ φ₃
τ : PropAssignment ν✝
⊢ eval τ φ₁ ≤ eval τ (conj φ₂ φ₃)
ν✝ : Type u_1
φ₁ φ₂ φ₃ : PropFun ν✝
h₁ : entails φ₁ φ₂
h₂ : entails φ₁ φ₃
τ : PropAssignment ν✝
⊢ eval τ φ₁ ≤ (eval τ φ₂ && eval τ φ₃)