Theorem neeq2 2996

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 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2	1	neeq2d 2993	1 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-cleq 2716  df-ne 2933

This theorem is referenced by:  psseq2  4081  prproe  4898  fprg  7146  f1dom3el3dif  7261  f1prex  7275  xpord2lem  8123  xpord3lem  8130  dfac5  10120  kmlem4  10145  kmlem14  10155  1re  11212  hashge2el2difr  14440  hashdmpropge2  14442  dvdsle  16252  sgrp2rid2ex  18844  isirred  20313  isnzr2  20412  dmatelnd  22322  mdetdiaglem  22424  mdetunilem1  22438  mdetunilem2  22439  maducoeval2  22466  hausnei  23156  regr1lem2  23568  xrhmeo  24795  axtg5seg  28188  axtgupdim2  28194  axtgeucl  28195  ishlg  28325  tglnpt2  28364  axlowdim1  28689  umgrvad2edg  28942  2pthdlem1  29656  3pthdlem1  29889  upgr3v3e3cycl  29905  upgr4cycl4dv4e  29910  eupth2lem3lem4  29956  3cyclfrgrrn1  30010  4cycl2vnunb  30015  numclwwlkovh  30098  numclwwlkovq  30099  numclwwlk2lem1  30101  numclwlk2lem2f  30102  superpos  32079  signswch  34064  axtgupdim2ALTV  34171  dfrdg4  35419  fvray  35609  linedegen  35611  fvline  35612  linethru  35621  hilbert1.1  35622  knoppndvlem21  35899  poimirlem1  36983  hlsuprexch  38746  3dim1lem5  38831  llni2  38877  lplni2  38902  2llnjN  38932  lvoli2  38946  2lplnj  38985  islinei  39105  cdleme40n  39833  cdlemg33b  40072  ax6e2ndeq  43834  ax6e2ndeqVD  44184  ax6e2ndeqALT  44206  refsum2cnlem1  44235  stoweidlem43  45269  nnfoctbdjlem  45681  elprneb  46249  ichnreuop  46650  inlinecirc02plem  47685