## Stream: new members

### Topic: Can't get basic proof of transitivity of P -> Q to work out:

#### Daniel Donnelly (May 22 2023 at 01:51):

example : (P → Q) → (Q → R) → (P → R) := by
intro hPQ
intro hQR
intro hP
apply (hPQ hP)


image.png

#### Mario Carneiro (May 22 2023 at 01:56):

hPQ hP is a proof of Q, you are trying to apply it when the goal is R

#### Mario Carneiro (May 22 2023 at 01:56):

(observe also that hQR is unused in this proof)

#### Mario Carneiro (May 22 2023 at 01:57):

if you meant to assert Q and add it to your context instead of trying to apply it to the goal, write

have hQ := hPQ hP


#### Daniel Donnelly (May 22 2023 at 02:01):

@Mario Carneiro With your help, I fixed it. Here it is:

example : (P → Q) → (Q → R) → (P → R) := by
intro hPQ
intro hQR
intro hP
have hQ := hPQ hP
have hR := hQR hQ
exact hR


#### Mario Carneiro (May 22 2023 at 02:02):

A proof using apply works backwards from the end:

example : (P → Q) → (Q → R) → (P → R) := by
intro hPQ
intro hQR
intro hP
apply hQR
apply hPQ
exact hP
`

#### Daniel Donnelly (May 22 2023 at 02:12):

@Mario Carneiro I will try that proof out to make sure I understand apply

Last updated: Dec 20 2023 at 11:08 UTC