case mp_ h1_phi h1_psi _ _ h1_ih_1 h1_ih_2 =>
  exact IsDeduct.mp_ h1_phi h1_psi h1_ih_1 h1_ih_2
F : Formula
Δ Γ : Set Formula
h2 : ∀ H ∈ Γ, IsDeduct Δ H
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Γ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Γ h1_phi
h1_ih_1 : IsDeduct Δ (h1_phi.imp_ h1_psi)
h1_ih_2 : IsDeduct Δ h1_phi
⊢ IsDeduct Δ h1_psi
no goals