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  6502  tfrcllemsucaccv  6515  enpr2d  6992  djune  7271  omp1eomlem  7287  difinfsn  7293  nnnninfeq2  7322  nninfisol  7326  netap  7466  2omotaplemap  7469  exmidapne  7472  xaddf  10072  xaddval  10073  xleaddadd  10115  flqltnz  10540  zfz1iso  11098  bezoutlemle  12572  eucalgval2  12618  eucalglt  12622  isprm2  12682  sqne2sq  12742  nnoddn2prmb  12828  ennnfonelemim  13038  ctinfomlemom  13041  hashfinmndnn  13508  logbgcd1irraplemexp  15685  lgsfcl2  15728  lgscllem  15729  lgsval2lem  15732  uhgr2edg  16050  bj-charfunbi  16356  3dom  16537  pw1ndom3lem  16538  nnsf  16557  peano3nninf  16559  neapmkvlem  16621