Theorem neeq2 2728

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

Assertion

Ref	Expression
neeq2	|- ( A = B -> ( C =/= A <-> C =/= B ) )

Proof of Theorem neeq2

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( A = B -> A = B )
2	1	neeq2d 2723	1 |- ( A = B -> ( C =/= A <-> C =/= B ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1370   =/= wne 2641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-12 1793  ax-ext 2429

This theorem depends on definitions:  df-bi 185  df-ex 1588  df-cleq 2442  df-ne 2643

This theorem is referenced by:  neeq2iOLD  2733  neeq2dOLD  2737  psseq2  3528  fprg  5976  f1dom3el3dif  6066  dfac5  8385  kmlem4  8409  kmlem14  8419  1re  9472  dvdsle  13666  isirred  16883  isnzr2  17437  mdetdiaglem  18506  mdetunilem1  18520  mdetunilem2  18521  maducoeval2  18548  hausnei  19034  regr1lem2  19415  xrhmeo  20620  axtg5seg  23028  axtgupdim2  23035  axtgeucl  23036  tglnpt2  23154  axlowdim1  23326  2pthoncl  23623  superpos  25879  signswch  27082  dfrdg4  28101  fvray  28292  linedegen  28294  fvline  28295  linethru  28304  hilbert1.1  28305  refsum2cnlem1  29883  stoweidlem43  29962  clwlknclwlkdifs  30702  3cyclfrgrarn1  30728  4cycl2vnunb  30733  numclwwlk2lem1  30819  numclwlk2lem2f  30820  dmatelnd  31015  dmatsubcl  31017  ax6e2ndeq  31550  ax6e2ndeqVD  31927  ax6e2ndeqALT  31949  hlsuprexch  33307  3dim1lem5  33392  llni2  33438  lplni2  33463  2llnjN  33493  lvoli2  33507  2lplnj  33546  islinei  33666  cdleme40n  34394  cdlemg33b  34633