Many axiom systems for propositional logic contain the following two axioms:
$1. (\phi_1\to(\phi_2\to\phi_1))$
$2. ((\phi_1\to(\phi_2\to\phi_3))\to((\phi_1\to\phi_2)\to(\phi_1\to\phi_3)))$
These two axioms are of interest in that they suffice to prove the Deduction Theorem.
I was wondering if there are any names for these axioms. On Metamath I see that the first one was referred to as the 'principle of simplification' by Russell and Whitehead. The second one is listed there simply as 'Frege' ... it was one of the axioms in Frege's original axiom system, but Russell and Whitehead derived it from their own axioms. .. but apparently none of them gave this axiom a proper name.
Has anyone seen any other names for these? Or if there really isn't much in the existing literature: can anyone think of some nice name! I must say that 1 doesn't strike me as a kind of 'simplification' .. maybe something more like 'conditionalization'. And in 2 I see a kind of 'embedded' or 'conditionalized' Modus Ponens. Anyway, I would be happy to hear your thoughts, thanks!!