I try to undestand the generalized tautology theorem (not sure wether it's the correct english expression) and its proof.

Doesn't it simply state the completeness of the axiom system (if it holds forall phi1..n)?

In the proof there is a curious step. It states that viamodus ponensyou can transform the first in the second statement:

I undestand the transformation, but I don't see modus ponens applied here. Anyone knows?

ps: Btw, where can I look up translations of mathematical expressions (e.g. completeness/Vollständigkeit,...) for English/German? I'm not used doing mathematics in English