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 ¬ ( 𝐴 = 𝐵𝐴𝐵 )