/sci/ - Science & Math

I'm confused with how line 5 works in this proof.
Where has ¬A come from? How can ¬A be justified when it has not been assumed?

It uses classical contradiction which I still don't fully understand so I'm hoping someone here knows how it works.