Applying to hypotheses

Stream: new members

[Ben Nale]

Suppose I have a hypothesis h1:H and a proof that H --> P (called HtoP). How do I change h1 to P?
What I would do is have h2:P, exact HtoP h1,
There's got to be another way.

Thanks

[Ben Nale]

hmmm. I can just make a lemma thats an iff and do rw.

[Ben Nale]

example (H P: Prop) (h1: H) : H → P ↔ P:=

[Kevin Buzzard]

replace h1 := HtoP h1

[Ben Nale]

nice :) thanks

[Bhavik Mehta]

(deleted)

[Ben Nale]

Thanks