Theorem axc5c4c711toc5

Description: Rederivation of sp from axc5c4c711 . Note that ax6 is used for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011) Revised to use ax6v instead of ax6 , so that this rederivation requires only ax6v and propositional calculus. (Revised by BJ, 14-Sep-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	axc5c4c711toc5	$$⊢\forall x\phi \to \phi$$

Proof

Step	Hyp	Ref	Expression
1		ax6v	$$⊢\neg \forall x\neg x=y$$
2		pm2.21	$$⊢\neg \phi \to \left(\phi \to \forall x\left(\forall x\phi \to \neg x=y\right)\right)$$
3		ax-1	$$⊢\left(\phi \to \forall x\left(\forall x\phi \to \neg x=y\right)\right)\to \left(\forall x\forall x\neg \forall x\forall x\left(\forall x\phi \to \neg x=y\right)\to \left(\phi \to \forall x\left(\forall x\phi \to \neg x=y\right)\right)\right)$$
4		axc5c4c711	$$⊢\left(\forall x\forall x\neg \forall x\forall x\left(\forall x\phi \to \neg x=y\right)\to \left(\phi \to \forall x\left(\forall x\phi \to \neg x=y\right)\right)\right)\to \left(\forall x\phi \to \forall x\neg x=y\right)$$
5	2 3 4	3syl	$$⊢\neg \phi \to \left(\forall x\phi \to \forall x\neg x=y\right)$$
6	1 5	mtoi	$$⊢\neg \phi \to \neg \forall x\phi$$
7	6	con4i	$$⊢\forall x\phi \to \phi$$