Theorem: ClassicalPropositionalLogic.valid_of_provable (GlimpseOfLean/Solutions/Topics/ClassicalPropositionalLogic.lean)

State before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h : Provable A
⊢ Valid A
Tactic:
exact soundness_theorem h
State after:
no goals