Theorem bj-ax6elem1

Description: Lemma for bj-ax6e . (Contributed by BJ, 22-Dec-2020) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-ax6elem1	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		axc9	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) ) )
2		axc16	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) )
3	1 2	pm2.61d2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑦 = 𝑧 → ∀ 𝑥 𝑦 = 𝑧 ) )