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  6612  tfrcllemsucaccv  6625  enpr2d  7111  djune  7418  omp1eomlem  7434  difinfsn  7440  nnnninfeq2  7469  nninfisol  7473  netap  7620  2omotaplemap  7623  exmidapne  7626  xaddf  10248  xaddval  10249  xleaddadd  10291  flqltnz  10724  zfz1iso  11295  hashtpglem  11300  bezoutlemle  12787  eucalgval2  12833  eucalglt  12837  isprm2  12897  sqne2sq  12957  nnoddn2prmb  13043  ballotfilemi1  13247  ballotfilemii  13248  ballotfilemfrcn0  13275  ennnfonelemim  13317  ctinfomlemom  13320  hashfinmndnn  13747  aprnzr  14601  logbgcd1irraplemexp  16076  lgsfcl2  16137  lgscllem  16138  lgsval2lem  16141  uhgr2edg  16459  eulerpathprum  16733  bj-charfunbi  16849  3dom  17030  pw1ndom3lem  17031  nnsf  17060  peano3nninf  17062  qdiff  17110  neapmkvlem  17129