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

Metamath Proof Explorer

Theorem nonconne

Description: Law of noncontradiction with equality and inequality. (Contributed by NM, 3-Feb-2012) (Proof shortened by Wolf Lammen, 21-Dec-2019)

Ref Expression
Assertion nonconne ¬ ( 𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐵 )

Proof

Step Hyp Ref Expression
1 fal ⊢ ¬ ⊥
2 eqneqall ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ≠ 𝐵 → ⊥ ) )
3 2 imp ⊢ ( ( 𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐵 ) → ⊥ )
4 1 3 mto ⊢ ¬ ( 𝐴 = 𝐵 ∧ 𝐴 ≠ 𝐵 )