Hilbert-Bernays-Löb derivability condition $\mathbf{D2}$

theorem LO.FirstOrder.Arithmetic.Bootstrapping.modus_ponens {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] {φ ψ : SyntacticFormula L} (hφψ : T.Provable ⌜φ ➝ ψ⌝) (hφ : T.Provable ⌜φ⌝) : T.Provable ⌜ψ⌝

Hilbert–Bernays provability condition D2

theorem LO.FirstOrder.Arithmetic.Bootstrapping.modus_ponens_sentence {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] {σ τ : Sentence L} (hστ : T.Provable ⌜σ ➝ τ⌝) (hσ : T.Provable ⌜σ⌝) : T.Provable ⌜τ⌝