How does (wikipedia's axiomatization of) intuitionistic logic prove $p \rightarrow p$? I'm looking at Wikipedia's article on Intuitionist logic, and I can't figure out how it would prove $(p \rightarrow p)$.
Does it prove $(p \rightarrow p)$?  If yes, how?
If no, is there a correct (or reasonable, if there is no "correct") axiomatization of intuitionistic logic available anywhere online?

*

*$p→(p→p)$ (THEN-1)  

*$p→((p→p)→p)$ (THEN-1)  

*$(p→((p→p)→p))→((p→(p→p))→(p→p))$ (THEN-2)  

*$(p→(p→p))→(p→p)$ (MP from lines 2,3)  

*$(p→p)$ (MP from lines 1,4)  

