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$$