Description: Over minimal implicational calculus, Peirce's axiom peirce implies an
axiom sometimes called "Roll",
( ( ( ph -> ps ) -> ch ) -> ( ( ch -> ph ) -> ph ) ) , of which
looinv is a special instance. The converse also holds: substitute
( ph -> ps ) for ch in Roll and use id and ax-mp .
(Contributed by BJ, 15-Jun-2021)