I have a problem understanding how modus ponens work when trying to deduce proof using already made axioms to formulas we want to prove that it is valid. This is the list of axioms:
α→β→α
(α→β→γ)→(α→β)→α→γ
α→β→(α∧β)
(α∧β)→α
(α∧β)→β
α→(α∨β)
β→(α∨β)
(α→γ)→(β→γ)→(α∨β)→γ
(α→β)→(α→¬β)→¬α
¬¬α→α
⊥→α
α→⊤
https://members.loria.fr/pdeGroote/logic/logic13.html
the link in the very end of the page shows a formula proved using axioms with modus ponens but I did not understand how they go from a step to another step. I know that modes is just inference rule but the shift from premise to conclusion is totally ambiguous. for example: how would we decide whether this formula is valid or not using the axioms with modus ponens. I know we can use truth tables. But this one got me truly perplexed.
((A → B) → A) → A