Theorem: Sat.limplies.trans (LeanSAT/Sat/Basic.lean)

State before:
α : Type u
σ1 : Type v
σ2 : Type w
σ3 : Type x
inst✝² : HSat α σ1
inst✝¹ : HSat α σ2
inst✝ : HSat α σ3
f1 : σ1
f2 : σ2
f3 : σ3
⊢ limplies α f1 f2 → limplies α f2 f3 → limplies α f1 f3
Tactic:
intros f1_implies_f2 f2_implies_f3 p p_entails_f1
State after:
α : Type u
σ1 : Type v
σ2 : Type w
σ3 : Type x
inst✝² : HSat α σ1
inst✝¹ : HSat α σ2
inst✝ : HSat α σ3
f1 : σ1
f2 : σ2
f3 : σ3
f1_implies_f2 : limplies α f1 f2
f2_implies_f3 : limplies α f2 f3
p : α → Bool
p_entails_f1 : p ⊨ f1
⊢ p ⊨ f3

State before:
α : Type u
σ1 : Type v
σ2 : Type w
σ3 : Type x
inst✝² : HSat α σ1
inst✝¹ : HSat α σ2
inst✝ : HSat α σ3
f1 : σ1
f2 : σ2
f3 : σ3
f1_implies_f2 : limplies α f1 f2
f2_implies_f3 : limplies α f2 f3
p : α → Bool
p_entails_f1 : p ⊨ f1
⊢ p ⊨ f3
Tactic:
exact f2_implies_f3 p $ f1_implies_f2 p p_entails_f1
State after:
no goals