Theorem: PropositionalLogic.HilbertSystem.HPM₀.id (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
φ : L
⊢ φ ∈ {φ}
Tactic:
simp
State after:
no goals