Description: Closed form for a1d . Deduction introducing an embedded antecedent.
Identical to rp-frege24 which was proved without relying on
ax-frege8 . Proposition 24 of Frege1879 p. 42. (Contributed by RP, 24-Dec-2019)(Proof modification is discouraged.)