Theorem neqned 2407

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1395   ≠ wne 2400

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 2401

This theorem is referenced by:  neqne  2408  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  enpr2d  6980  djune  7253  omp1eomlem  7269  difinfsn  7275  nnnninfeq2  7304  nninfisol  7308  netap  7448  2omotaplemap  7451  exmidapne  7454  xaddf  10048  xaddval  10049  xleaddadd  10091  flqltnz  10515  zfz1iso  11071  bezoutlemle  12537  eucalgval2  12583  eucalglt  12587  isprm2  12647  sqne2sq  12707  nnoddn2prmb  12793  ennnfonelemim  13003  ctinfomlemom  13006  hashfinmndnn  13473  logbgcd1irraplemexp  15650  lgsfcl2  15693  lgscllem  15694  lgsval2lem  15697  uhgr2edg  16012  bj-charfunbi  16198  3dom  16381  pw1ndom3lem  16382  nnsf  16401  peano3nninf  16403  neapmkvlem  16465