Theorem neqned 2427

Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2441. One-way deduction form of df-ne 2421. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2470. (Revised by Wolf Lammen, 22-Nov-2019.)

Hypothesis

Ref	Expression
neqned.1	⊢ (𝜑 → ¬ 𝐴 = 𝐵)

Assertion

Ref	Expression
neqned	⊢ (𝜑 → 𝐴 ≠ 𝐵)

Proof of Theorem neqned

Step	Hyp	Ref	Expression
1		neqned.1	. 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
2		df-ne 2421	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	sylibr 134	1 ⊢ (𝜑 → 𝐴 ≠ 𝐵)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1402   ≠ wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-ne 2421

This theorem is used by:  neqne  2428  tfr1onlemsucaccv  6617  tfrcllemsucaccv  6630  enpr2d  7117  djune  7425  omp1eomlem  7441  difinfsn  7447  nnnninfeq2  7476  nninfisol  7480  netap  7627  2omotaplemap  7630  exmidapne  7633  xaddf  10263  xaddval  10264  xleaddadd  10306  flqltnz  10743  zfz1iso  11315  hashtpglem  11320  bezoutlemle  12810  eucalgval2  12856  eucalglt  12860  isprm2  12920  sqne2sq  12982  sqrtrirr  13014  nnoddn2prmb  13070  ballotfilemi1  13303  ballotfilemii  13304  ballotfilemfrcn0  13331  ennnfonelemim  13373  ctinfomlemom  13376  hashfinmndnn  13804  aprnzr  14708  logbgcd1irraplemexp  16237  lgsfcl2  16363  lgscllem  16364  lgsval2lem  16367  uhgr2edg  16685  eulerpathprum  16959  bj-charfunbi  17075  3dom  17256  pw1ndom3lem  17257  nnsf  17287  peano3nninf  17289  qdiff  17338  neapmkvlem  17357