Disjunctive syllogism

Stream: new members

[Luiz Kazuo Takei]

I have the impression I saw this somewhere but I cannot find it. Suppose I have

h1 : ¬ P
h2 : P ∨ Q

is there a single lemma that allows me combine them to produce Q?

[Aaron Liu]

docs#Or.resolve_left

[Luiz Kazuo Takei]

Thanks!