This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem naev2

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

		Ref	Expression
	Assertion	naev2	$⊢ \neg \forall x x = y \to \forall z \neg \forall t t = u$

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