Theorem neqned 2384

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1373   ≠ wne 2377

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 2378

This theorem is referenced by:  neqne  2385  tfr1onlemsucaccv  6434  tfrcllemsucaccv  6447  enpr2d  6918  djune  7187  omp1eomlem  7203  difinfsn  7209  nnnninfeq2  7238  nninfisol  7242  netap  7373  2omotaplemap  7376  exmidapne  7379  xaddf  9973  xaddval  9974  xleaddadd  10016  flqltnz  10437  zfz1iso  10993  bezoutlemle  12373  eucalgval2  12419  eucalglt  12423  isprm2  12483  sqne2sq  12543  nnoddn2prmb  12629  ennnfonelemim  12839  ctinfomlemom  12842  hashfinmndnn  13308  logbgcd1irraplemexp  15484  lgsfcl2  15527  lgscllem  15528  lgsval2lem  15531  bj-charfunbi  15821  nnsf  16016  peano3nninf  16018  neapmkvlem  16080