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.Δ₁] {φ ψ : Proposition L} (hφψ : Provable T ⌜φ 🡒 ψ⌝) (hφ : Provable T ⌜φ⌝) : Provable T ⌜ψ⌝

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στ : Provable T ⌜σ 🡒 τ⌝) (hσ : Provable T ⌜σ⌝) : Provable T ⌜τ⌝