Drop a premise in a goal in apply style

Question

let's assume I want to show the following lemma

lemma "⟦ A; B; C ⟧ ⟹ D"

I get the goal

1. A ⟹ B ⟹ C ⟹ D

However, I don't need B. How can I transfer my goal to something like

1. A ⟹ C ⟹ D

I don't want to alter the original lemma statement, just the current goal in apply style.

Answer 1

What you want is apply (thin_tac B). However, the last time I did this, Peter Lammich shouted "Oh god, why are you doing this!" in disgust and rewrote my proof in order to get rid of the thin_tac. So using this tactic doesn't exactly seem to be encouraged anymore.