Degenerate instance of [ax-13] where bundled variables \( x \), \( y \), and \( z \) have a common substitution. Therefore, also a degenerate instance of ax13dgen1, ax13dgen2, and ax13dgen3. Also an instance of the intuitionistic tautology pm2.21. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 13-Apr-2017.) Reduce axiom usage. (Revised by Wolf Lammen, 10-Oct-2021.)