Theorem: LeanSAT.Model.PropFun.entails_conj (LeanSAT/Model/PropFun.lean)

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

State before:
ν✝ : Type u_1
φ₁ φ₂ φ₃ : PropFun ν✝
h₁ : entails φ₁ φ₂
h₂ : entails φ₁ φ₃
τ : PropAssignment ν✝
⊢ eval τ φ₁ ≤ (eval τ φ₂ && eval τ φ₃)
Tactic:
exact le_inf (h₁ τ) (h₂ τ)
State after:
no goals