Theorem neeq2 3022

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 3019	1 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ≠ wne 2959

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ne 2960

This theorem is used by:  psseq2  4021  prproe  4838  fprg  7191  f1dom3el3dif  7304  f1ounsn  7311  f1prex  7323  resf1extb  7980  xpord2lem  8196  xpord3lem  8203  dfac5  10246  kmlem4  10271  kmlem14  10281  1re  11347  hashge2el2difr  14667  hashdmpropge2  14669  dvdsle  16524  sgrp2rid2ex  19176  isirred  20700  isnzr2  20819  dmatelnd  22866  mdetdiaglem  22968  mdetunilem1  22982  mdetunilem2  22983  maducoeval2  23010  hausnei  23701  regr1lem2  24114  xrhmeo  25322  axtg5seg  28984  axtgupdim2  28990  axtgeucl  28991  ishlg2  29122  ishlg  29125  tglnpt2  29178  elcgrabasi  29432  axlowdim1  29594  umgrvad2edg  29851  2pthdlem1  30576  3pthdlem1  30822  upgr3v3e3cycl  30838  upgr4cycl4dv4e  30843  eupth2lem3lem4  30889  3cyclfrgrrn1  30943  4cycl2vnunb  30948  numclwwlkovh  31031  numclwwlkovq  31032  numclwwlk2lem1  31034  numclwlk2lem2f  31035  superpos  33013  constrconj  34488  constrcccllem  34497  constrcbvlem  34498  signswch  35301  axtgupdim2ALTV  35408  gdlopcfvlem  36012  dfrdg4  36930  fvray  37121  linedegen  37123  fvline  37124  linethru  37133  hilbert1.1  37134  knoppndvlem21  37613  qdiff  38516  poimirlem1  38807  hlsuprexch  40704  3dim1lem5  40789  llni2  40835  lplni2  40860  2llnjN  40890  lvoli2  40904  2lplnj  40943  islinei  41063  cdleme40n  41791  cdlemg33b  42030  ax6e2ndeq  45802  ax6e2ndeqVD  46151  ax6e2ndeqALT  46173  permac8prim  46268  refsum2cnlem1  46328  stoweidlem43  47326  nnfoctbdjlem  47738  elprneb  48372  ichnreuop  48827  usgrgrtrirex  49321  gpg5nbgrvtx03starlem1  49439  gpg5nbgrvtx03starlem3  49441  gpg5nbgrvtx13starlem1  49442  gpg5nbgrvtx13starlem3  49444  gpg3kgrtriex  49460  inlinecirc02plem  50229  oppcthinendcALT  50907