Theorem: Metamath.Statement.provable.trim (Metamath/Translate.lean)

State before:
axs : Statement → Prop
s : Statement
⊢ provable axs (Statement.trim s) ↔ provable axs s
Tactic:
simp only [provable, untrim_trim]
State after:
no goals