I can't figure out how to prove that formally. Please, help!!
Here is a way to prove this using the rules in Klement's Fitch-style proof checker. The rules are described in forallx. Both are available in the links below and would make good supplementary material to whatever text you are using.
This proof uses the law of the excluded middle (LEM). To use this I take a simple statement and its negation and from both try to derive the same result. If I get the same result than I can invoke the law of the excluded middle. Here I chose "P" and "¬P", because one of these, "P", is the goal itself.
For "P" I need do nothing but add the subproof with assumption "P". For "¬P" I use disjunction introduction to get line 4 and then conditional elimination on line 5 (modus ponens) to get "P". I reached the goal, "P", in both cases and so I can discharge the two assumptions on line 2 and 3 and reach the end of the proof.
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/