Theorem neqned 2419

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1398   ≠ wne 2412

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 2413

This theorem is referenced by:  neqne  2420  tfr1onlemsucaccv  6571  tfrcllemsucaccv  6584  enpr2d  7063  djune  7368  omp1eomlem  7384  difinfsn  7390  nnnninfeq2  7419  nninfisol  7423  netap  7564  2omotaplemap  7567  exmidapne  7570  xaddf  10173  xaddval  10174  xleaddadd  10216  flqltnz  10643  zfz1iso  11206  hashtpglem  11211  bezoutlemle  12697  eucalgval2  12743  eucalglt  12747  isprm2  12807  sqne2sq  12867  nnoddn2prmb  12953  ennnfonelemim  13164  ctinfomlemom  13167  hashfinmndnn  13634  logbgcd1irraplemexp  15820  lgsfcl2  15866  lgscllem  15867  lgsval2lem  15870  uhgr2edg  16188  eulerpathprum  16462  bj-charfunbi  16568  3dom  16749  pw1ndom3lem  16750  nnsf  16770  peano3nninf  16772  qdiff  16820  neapmkvlem  16839