Weakening of [ax-1]. As a consequence, its associated inference is an instance (where we allow extra hypotheses) of [ax-1]. Its commuted form is 2a1 (but ax1w does not require [ax-2] ). (Contributed by BJ, 11-Aug-2020.)
Weakening of [ax-1]. As a consequence, its associated inference is an instance (where we allow extra hypotheses) of [ax-1]. Its commuted form is 2a1 (but ax1w does not require [ax-2] ). (Contributed by BJ, 11-Aug-2020.)