Theorem naev2

Generalization of hbnaev. (Contributed by Wolf Lammen, 9-Apr-2021.)

Conclusion
\( \vdash \neg \forall x \, x = y' \rightarrow \forall z \, \neg \forall t \, t = u' \)
Proof
l0
naev
\( \vdash \neg \forall x \, x = y' \rightarrow \neg \forall v \, v = w \)
l1
ax-5
\( \vdash \neg \forall v \, v = w \rightarrow \forall z \, \neg \forall v \, v = w \)
naev
alimi _
\( \vdash \forall z \, \neg \forall v \, v = w \rightarrow \forall z \, \neg \forall t \, t = u' \)
3syl l0 l1 _