Theorem: PropositionalLogic.HilbertSystem.HPM₀.weakenImp (PropositionalLogic/HilbertSystem/HPM₀.lean)

State before:
L : Type u
inst✝⁵ : DecidableEq L
inst✝⁴ : HasArrow L
inst✝³ : HasBot L
inst✝² : HasLnot L
inst✝¹ : HilbertSystem L
inst✝ : HPM₀ L
Γ : Finset L
ψ φ : L
⊢ (Γ ⊢ ψ) → (Γ ⊢ φ →' ψ)
Tactic:
exact λ h => MP (axiomK _ ψ φ) h
State after:
no goals