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

Metamath Proof Explorer

Theorem bj-ax6elem1

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

Ref Expression
Assertion bj-ax6elem1 ⊢ ¬ ∀ x x = y → y = z → ∀ x y = z

Proof

Step Hyp Ref Expression
1 axc9 ⊢ ¬ ∀ x x = y → ¬ ∀ x x = z → y = z → ∀ x y = z
2 axc16 ⊢ ∀ x x = z → y = z → ∀ x y = z
3 1 2 pm2.61d2 ⊢ ¬ ∀ x x = y → y = z → ∀ x y = z