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  6498  tfrcllemsucaccv  6511  enpr2d  6985  djune  7261  omp1eomlem  7277  difinfsn  7283  nnnninfeq2  7312  nninfisol  7316  netap  7456  2omotaplemap  7459  exmidapne  7462  xaddf  10057  xaddval  10058  xleaddadd  10100  flqltnz  10524  zfz1iso  11081  bezoutlemle  12550  eucalgval2  12596  eucalglt  12600  isprm2  12660  sqne2sq  12720  nnoddn2prmb  12806  ennnfonelemim  13016  ctinfomlemom  13019  hashfinmndnn  13486  logbgcd1irraplemexp  15663  lgsfcl2  15706  lgscllem  15707  lgsval2lem  15710  uhgr2edg  16025  bj-charfunbi  16283  3dom  16465  pw1ndom3lem  16466  nnsf  16485  peano3nninf  16487  neapmkvlem  16549