Theorem neqned 2367

Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2381. One-way deduction form of df-ne 2361. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2410. (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 2361	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	sylibr 134	1 ⊢ (𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1364   ≠ wne 2360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-ne 2361

This theorem is referenced by:  neqne  2368  tfr1onlemsucaccv  6360  tfrcllemsucaccv  6373  enpr2d  6835  djune  7095  omp1eomlem  7111  difinfsn  7117  nnnninfeq2  7145  nninfisol  7149  netap  7271  2omotaplemap  7274  exmidapne  7277  xaddf  9862  xaddval  9863  xleaddadd  9905  flqltnz  10305  zfz1iso  10839  bezoutlemle  12027  eucalgval2  12071  eucalglt  12075  isprm2  12135  sqne2sq  12195  nnoddn2prmb  12280  ennnfonelemim  12443  ctinfomlemom  12446  hashfinmndnn  12859  logbgcd1irraplemexp  14783  lgsfcl2  14804  lgscllem  14805  lgsval2lem  14808  bj-charfunbi  14960  nnsf  15152  peano3nninf  15154  neapmkvlem  15213