Löb proved the following: for any C, Provable(Provable(C)->C)->Provable(C).
So, we may derive from PA soundness, that for any C, Provable(Provable(C)->C)->C.
Nobody proved, as you stated, that for any C (Provable(C)->C)->C.
Löb proved the following: for any C, Provable(Provable(C)->C)->Provable(C).
So, we may derive from PA soundness, that for any C, Provable(Provable(C)->C)->C.
Nobody proved, as you stated, that for any C (Provable(C)->C)->C.