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  6616  tfrcllemsucaccv  6629  enpr2d  7116  djune  7425  omp1eomlem  7441  difinfsn  7447  nnnninfeq2  7476  nninfisol  7480  netap  7627  2omotaplemap  7630  exmidapne  7633  xaddf  10264  xaddval  10265  xleaddadd  10307  flqltnz  10744  zfz1iso  11316  hashtpglem  11321  bezoutlemle  12811  eucalgval2  12857  eucalglt  12861  isprm2  12921  sqne2sq  12983  sqrtrirr  13015  nnoddn2prmb  13071  ballotfilemi1  13304  ballotfilemii  13305  ballotfilemfrcn0  13332  ennnfonelemim  13374  ctinfomlemom  13377  hashfinmndnn  13805  aprnzr  14709  logbgcd1irraplemexp  16216  lgsfcl2  16342  lgscllem  16343  lgsval2lem  16346  uhgr2edg  16664  eulerpathprum  16938  bj-charfunbi  17054  3dom  17235  pw1ndom3lem  17236  nnsf  17266  peano3nninf  17268  qdiff  17317  neapmkvlem  17336