Theorem neqned 2427

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1402   ≠ wne 2420

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 2421

This theorem is referenced by:  neqne  2428  tfr1onlemsucaccv  6606  tfrcllemsucaccv  6619  enpr2d  7105  djune  7412  omp1eomlem  7428  difinfsn  7434  nnnninfeq2  7463  nninfisol  7467  netap  7614  2omotaplemap  7617  exmidapne  7620  xaddf  10229  xaddval  10230  xleaddadd  10272  flqltnz  10705  zfz1iso  11276  hashtpglem  11281  bezoutlemle  12768  eucalgval2  12814  eucalglt  12818  isprm2  12878  sqne2sq  12938  nnoddn2prmb  13024  ballotfilemi1  13228  ballotfilemii  13229  ballotfilemfrcn0  13256  ennnfonelemim  13298  ctinfomlemom  13301  hashfinmndnn  13728  aprnzr  14582  logbgcd1irraplemexp  16053  lgsfcl2  16108  lgscllem  16109  lgsval2lem  16112  uhgr2edg  16430  eulerpathprum  16704  bj-charfunbi  16820  3dom  17001  pw1ndom3lem  17002  nnsf  17022  peano3nninf  17024  qdiff  17072  neapmkvlem  17091