Theorem naev2

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

	Ref	Expression
Assertion	naev2	|- ( -. A. x x = y -> A. z -. A. t t = u )

Proof

Step	Hyp	Ref	Expression
1		naev	|- ( -. A. x x = y -> -. A. v v = w )
2		ax-5	|- ( -. A. v v = w -> A. z -. A. v v = w )
3		naev	|- ( -. A. v v = w -> -. A. t t = u )
4	3	alimi	|- ( A. z -. A. v v = w -> A. z -. A. t t = u )
5	1 2 4	3syl	|- ( -. A. x x = y -> A. z -. A. t t = u )