Theorem neeq2 3027

Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.)

Assertion

Ref	Expression
neeq2	⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))

Proof of Theorem neeq2

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	neeq2d 3024	1 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ≠ wne 2964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ne 2965

This theorem is referenced by:  psseq2  4053  prproe  4871  fprg  7150  f1dom3el3dif  7265  f1ounsn  7268  f1prex  7280  resf1extb  7927  xpord2lem  8134  xpord3lem  8141  dfac5  10108  kmlem4  10133  kmlem14  10143  1re  11204  hashge2el2difr  14514  hashdmpropge2  14516  dvdsle  16364  sgrp2rid2ex  18985  isirred  20497  isnzr2  20597  dmatelnd  22618  mdetdiaglem  22720  mdetunilem1  22734  mdetunilem2  22735  maducoeval2  22762  hausnei  23450  regr1lem2  23862  xrhmeo  25070  axtg5seg  28696  axtgupdim2  28702  axtgeucl  28703  ishlg  28833  tglnpt2  28884  axlowdim1  29246  umgrvad2edg  29500  2pthdlem1  30216  3pthdlem1  30452  upgr3v3e3cycl  30468  upgr4cycl4dv4e  30473  eupth2lem3lem4  30519  3cyclfrgrrn1  30573  4cycl2vnunb  30578  numclwwlkovh  30661  numclwwlkovq  30662  numclwwlk2lem1  30664  numclwlk2lem2f  30665  superpos  32643  constrconj  34076  constrcccllem  34085  constrcbvlem  34086  signswch  34889  axtgupdim2ALTV  34996  dfrdg4  36338  fvray  36528  linedegen  36530  fvline  36531  linethru  36540  hilbert1.1  36541  knoppndvlem21  37006  qdiff  37854  poimirlem1  38155  hlsuprexch  40040  3dim1lem5  40125  llni2  40171  lplni2  40196  2llnjN  40226  lvoli2  40240  2lplnj  40279  islinei  40399  cdleme40n  41127  cdlemg33b  41366  ax6e2ndeq  45155  ax6e2ndeqVD  45504  ax6e2ndeqALT  45526  permac8prim  45610  refsum2cnlem1  45644  stoweidlem43  46644  nnfoctbdjlem  47056  elprneb  47650  ichnreuop  48105  usgrgrtrirex  48599  gpg5nbgrvtx03starlem1  48717  gpg5nbgrvtx03starlem3  48719  gpg5nbgrvtx13starlem1  48720  gpg5nbgrvtx13starlem3  48722  gpg3kgrtriex  48738  inlinecirc02plem  49446  oppcthinendcALT  50099