exact (dn_distribute_imply'! $ ih₁ ⟨h₁⟩) ⨀ ih₂ ⟨h₂⟩
case mpr.mdp
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p✝ p q : Formula α
h₁ : Deduction 𝐂𝐥 (p ⟶ q)
h₂ : Deduction 𝐂𝐥 p
ih₁ : 𝐂𝐥 ⊢! p ⟶ q → 𝐈𝐧𝐭 ⊢! ~~(p ⟶ q)
ih₂ : 𝐂𝐥 ⊢! p → 𝐈𝐧𝐭 ⊢! ~~p
d : 𝐂𝐥 ⊢! q
⊢ 𝐈𝐧𝐭 ⊢! ~~q
no goals