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

Metamath Proof Explorer

Theorem axc5sp1

Description: A special case of ax-c5 without using ax-c5 or ax-5 . (Contributed by NM, 13-Jan-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	axc5sp1	$⊢ \forall y \neg x = x \to \neg x = x$

Proof

Step	Hyp	Ref	Expression
1		equidqe	$⊢ \neg \forall y \neg x = x$
2	1	pm2.21i	$⊢ \forall y \neg x = x \to \neg x = x$