Theorem neqned 2354

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1353   ≠ wne 2347

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 2348

This theorem is referenced by:  neqne  2355  tfr1onlemsucaccv  6342  tfrcllemsucaccv  6355  enpr2d  6817  djune  7077  omp1eomlem  7093  difinfsn  7099  nnnninfeq2  7127  nninfisol  7131  netap  7253  2omotaplemap  7256  exmidapne  7259  xaddf  9844  xaddval  9845  xleaddadd  9887  flqltnz  10287  zfz1iso  10821  bezoutlemle  12009  eucalgval2  12053  eucalglt  12057  lcmval  12063  lcmcllem  12067  isprm2  12117  sqne2sq  12177  nnoddn2prmb  12262  ennnfonelemim  12425  ctinfomlemom  12428  hashfinmndnn  12833  logbgcd1irraplemexp  14389  lgsfcl2  14410  lgscllem  14411  lgsval2lem  14414  bj-charfunbi  14566  nnsf  14757  peano3nninf  14759  neapmkvlem  14817