Theorem: PropositionalLogic.HilbertSystem.insertEmpty (PropositionalLogic/HilbertSystem/Definitions.lean)

State before:
L✝ : Type u
inst✝³ : DecidableEq L✝
inst✝² : HasMinimalLogicSymbols L✝
L : Type u
inst✝¹ : DecidableEq L
inst✝ : HilbertSystem L
ψ φ : L
⊢ ({φ} ⊢ ψ) → (∅ ∪ {φ} ⊢ ψ)
Tactic:
simp
State after:
no goals