Theorem neeq2 3018

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

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

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

This theorem is used by:  psseq2  4039  prproe  4865  fprg  7152  f1dom3el3dif  7266  f1ounsn  7273  f1prex  7285  resf1extb  7931  xpord2lem  8140  xpord3lem  8147  dfac5  10131  kmlem4  10156  kmlem14  10166  1re  11232  hashge2el2difr  14546  hashdmpropge2  14548  dvdsle  16400  sgrp2rid2ex  19039  isirred  20560  isnzr2  20678  dmatelnd  22718  mdetdiaglem  22820  mdetunilem1  22834  mdetunilem2  22835  maducoeval2  22862  hausnei  23553  regr1lem2  23966  xrhmeo  25174  axtg5seg  28806  axtgupdim2  28812  axtgeucl  28813  ishlg2  28944  ishlg  28947  tglnpt2  29000  elcgrabasi  29254  axlowdim1  29416  umgrvad2edg  29673  2pthdlem1  30398  3pthdlem1  30644  upgr3v3e3cycl  30660  upgr4cycl4dv4e  30665  eupth2lem3lem4  30711  3cyclfrgrrn1  30765  4cycl2vnunb  30770  numclwwlkovh  30853  numclwwlkovq  30854  numclwwlk2lem1  30856  numclwlk2lem2f  30857  superpos  32835  constrconj  34255  constrcccllem  34264  constrcbvlem  34265  signswch  35069  axtgupdim2ALTV  35176  dfrdg4  36530  fvray  36721  linedegen  36723  fvline  36724  linethru  36733  hilbert1.1  36734  knoppndvlem21  37229  qdiff  38079  poimirlem1  38370  hlsuprexch  40254  3dim1lem5  40339  llni2  40385  lplni2  40410  2llnjN  40440  lvoli2  40454  2lplnj  40493  islinei  40613  cdleme40n  41341  cdlemg33b  41580  ax6e2ndeq  45382  ax6e2ndeqVD  45731  ax6e2ndeqALT  45753  permac8prim  45837  refsum2cnlem1  45871  stoweidlem43  46871  nnfoctbdjlem  47283  elprneb  47917  ichnreuop  48372  usgrgrtrirex  48866  gpg5nbgrvtx03starlem1  48984  gpg5nbgrvtx03starlem3  48986  gpg5nbgrvtx13starlem1  48987  gpg5nbgrvtx13starlem3  48989  gpg3kgrtriex  49005  inlinecirc02plem  49716  oppcthinendcALT  50367