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	⊢ ( ∀ 𝑥 𝜑 → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		ax6v	⊢ ¬ ∀ 𝑥 ¬ 𝑥 = 𝑦
2		pm2.21	⊢ ( ¬ 𝜑 → ( 𝜑 → ∀ 𝑥 ( ∀ 𝑥 𝜑 → ¬ 𝑥 = 𝑦 ) ) )
3		ax-1	⊢ ( ( 𝜑 → ∀ 𝑥 ( ∀ 𝑥 𝜑 → ¬ 𝑥 = 𝑦 ) ) → ( ∀ 𝑥 ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑥 ( ∀ 𝑥 𝜑 → ¬ 𝑥 = 𝑦 ) → ( 𝜑 → ∀ 𝑥 ( ∀ 𝑥 𝜑 → ¬ 𝑥 = 𝑦 ) ) ) )
4		axc5c4c711	⊢ ( ( ∀ 𝑥 ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑥 ( ∀ 𝑥 𝜑 → ¬ 𝑥 = 𝑦 ) → ( 𝜑 → ∀ 𝑥 ( ∀ 𝑥 𝜑 → ¬ 𝑥 = 𝑦 ) ) ) → ( ∀ 𝑥 𝜑 → ∀ 𝑥 ¬ 𝑥 = 𝑦 ) )
5	2 3 4	3syl	⊢ ( ¬ 𝜑 → ( ∀ 𝑥 𝜑 → ∀ 𝑥 ¬ 𝑥 = 𝑦 ) )
6	1 5	mtoi	⊢ ( ¬ 𝜑 → ¬ ∀ 𝑥 𝜑 )
7	6	con4i	⊢ ( ∀ 𝑥 𝜑 → 𝜑 )