Description: 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)