Theorem naev2

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

	Ref	Expression
Assertion	naev2	$$⊢\neg \forall xx=y\to \forall z\neg \forall tt=u$$

Proof

Step	Hyp	Ref	Expression
1		naev	$$⊢\neg \forall xx=y\to \neg \forall vv=w$$
2		ax-5	$$⊢\neg \forall vv=w\to \forall z\neg \forall vv=w$$
3		naev	$$⊢\neg \forall vv=w\to \neg \forall tt=u$$
4	3	alimi	$$⊢\forall z\neg \forall vv=w\to \forall z\neg \forall tt=u$$
5	1 2 4	3syl	$$⊢\neg \forall xx=y\to \forall z\neg \forall tt=u$$