Theorem neeq1d 3000

Description: Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)

Hypothesis

Ref	Expression
neeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
neeq1d	⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Proof of Theorem neeq1d

Step	Hyp	Ref	Expression
1		neeq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eqeq1d 2739	. 2 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
3	2	necon3bid 2985	1 ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ≠ wne 2940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ne 2941

This theorem is referenced by:  neeq1  3003  eqnetrd  3008  iftrueb  4538  inisegn0  6116  f1ounsn  7292  f12dfv  7293  f13dfv  7294  resf1extb  7956  suppval1  8191  elsuppfng  8194  elsuppfn  8195  suppsnop  8203  ressuppss  8208  ressuppssdif  8210  tz7.49  8485  ereldm  8795  pw2f1olem  9116  marypha1lem  9473  wdomtr  9615  inf3lem2  9669  cantnflem1  9729  cantnf  9733  cplem2  9930  dfac9  10177  kmlem12  10202  infpssrlem4  10346  fin23lem14  10373  axcc2lem  10476  axcc3  10478  domtriomlem  10482  axdc2lem  10488  ac6c4  10521  zorn2lem6  10541  rpnnen1lem4  13022  rpnnen1lem5  13023  mptnn0fsuppr  14040  hashprg  14434  hashtpg  14524  prodfn0  15930  prodfrec  15931  prodfdiv  15932  ntrivcvgtail  15936  fproddiv  15997  fprodn0  16015  fproddivf  16023  dvdsle  16347  algcvg  16613  algcvga  16616  eucalgcvga  16623  rpdvds  16697  phibndlem  16807  dfphi2  16811  pcaddlem  16926  vdwmc  17016  iscatd2  17724  brcic  17842  cicer  17850  cat1lem  18141  cat1  18142  sgrp2nmndlem5  18942  symgextf1lem  19438  pmtrmvd  19474  frgpup3lem  19795  isirred  20419  rrgsupp  20701  isdrngrd  20766  isdrngrdOLD  20768  nzerooringczr  21491  dsmmelbas  21759  dsmmacl  21761  frlmssuvc2  21815  mhpsclcl  22151  mhpmulcl  22153  elcls  23081  clsndisj  23083  elcls3  23091  neindisj2  23131  clslp  23156  cmpfi  23416  cmpfii  23417  dfconn2  23427  connsuba  23428  nconnsubb  23431  1stcelcls  23469  finlocfin  23528  locfincmp  23534  dissnlocfin  23537  locfindis  23538  ptclsg  23623  dfac14lem  23625  isfbas  23837  trfbas2  23851  isfil  23855  filss  23861  fbunfip  23877  fgval  23878  elfg  23879  isufil2  23916  ufileu  23927  filufint  23928  fmfnfm  23966  flimclslem  23992  fclsopni  24023  fclsnei  24027  fclsbas  24029  fclsrest  24032  fclscmp  24038  ufilcmp  24040  isfcf  24042  fcfnei  24043  fcfneii  24045  ptcmplem2  24061  cnextcn  24075  cnextfres1  24076  tsmsfbas  24136  iscusp  24308  cuspcvg  24310  lpbl  24516  prdsxmslem2  24542  restmetu  24583  qdensere  24790  lebnumlem3  24995  isphtpc  25026  iscmet  25318  cmetcvg  25319  equivcmet  25351  cmetcusp1  25387  cmetcusp  25388  rrxmvallem  25438  ovolicc2lem2  25553  ovolicc2lem5  25556  i1fres  25740  lhop1lem  26052  deg1ldg  26131  plyco0  26231  plyeq0lem  26249  coeeq2  26281  coe1termlem  26297  taylfval  26400  cxpeq0  26720  ftalem4  27119  ftalem5  27120  ftalem6  27121  isppw  27157  isnsqf  27178  sqff1o  27225  musum  27234  dchrelbas3  27282  dchrelbasd  27283  dchrelbas4  27287  dchrmulcl  27293  dchrn0  27294  dchrfi  27299  dchrptlem2  27309  dchrpt  27311  lgsne0  27379  lgsdchr  27399  2sqlem11  27473  nosupbnd2lem1  27760  expsne0  28414  ishlg  28610  uvtx01vtx  29414  pthdlem2lem  29787  2pthdlem1  29950  clwwlknclwwlkdif  29998  umgr2cwwkdifex  30084  3pthdlem1  30183  frgrregorufr  30344  numclwwlk2lem1lem  30361  numclwwlk2lem1  30395  numclwlk2lem2f  30396  numclwlk2lem2f1o  30398  nmorepnf  30787  nmoprepnf  31886  nmfnrepnf  31899  fdifsupp  32694  ressupprn  32699  disjdsct  32712  rmfsupp2  33242  domnprodn0  33279  isufd  33568  ufdprmidl  33569  1arithufdlem4  33575  dfufd2lem  33577  fedgmullem2  33681  constrconj  33786  constrelextdg2  33788  locfinreflem  33839  sibfof  34342  signswch  34576  signstfvneq0  34587  derangenlem  35176  subfacp1lem3  35187  subfacp1lem5  35189  subfacp1lem6  35190  subfacp1  35191  iscvm  35264  cvmcov  35268  cvmcov2  35280  eldm3  35761  elima4  35776  neibastop1  36360  neibastop2lem  36361  neibastop2  36362  neibastop3  36363  neifg  36372  poimirlem17  37644  poimirlem18  37645  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem23  37650  poimirlem27  37654  poimirlem28  37655  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  mblfinlem3  37666  itg2addnclem3  37680  sstotbnd2  37781  cntotbnd  37803  heibor1lem  37816  dmecd  38305  disjecxrn  38390  br1cosscnvxrn  38475  2llnm3N  39571  dalem4  39667  cdlemk28-3  40910  mapdh9a  41791  idomnnzpownz  42133  idomnnzgmulnz  42134  sticksstones1  42147  aks6d1c6lem1  42171  unitscyglem2  42197  unitscyglem3  42198  unitscyglem4  42199  metakunt29  42234  readvcot  42394  domnexpgn0cl  42533  fsuppind  42600  dffltz  42644  pellexlem3  42842  mncn0  43151  aaitgo  43174  gneispace0nelrn2  44154  cvgdvgrat  44332  binomcxplemnotnn0  44375  disjf1  45188  disjrnmpt2  45193  disjinfi  45197  fsumiunss  45590  islptre  45634  islpcn  45654  lptre2pt  45655  0ellimcdiv  45664  liminflelimsup  45791  stoweidlem28  46043  stoweidlem43  46058  dirkercncflem2  46119  fourierdlem46  46167  fourierdlem79  46200  elaa2lem  46248  elaa2  46249  sge0fodjrnlem  46431  sge0iunmpt  46433  nnfoctbdjlem  46470  meadjiunlem  46480  meadjiun  46481  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem3  48029  ovn0ssdmfun  48075  rmsupp0  48284  scmsuppss  48287  suppmptcfin  48292  linc1  48342  el0ldep  48383  ldepspr  48390  islindeps2  48400  zlmodzxzldeplem4  48420  zlmodzxzldep  48421  ldepsnlinclem1  48422  ldepsnlinclem2  48423  ldepsnlinc  48425  fvconstr  48765  fvconstrn0  48766  fvconstr2  48767  catprslem  48899  catprsc  48902  catprsc2  48903  secval  49266  cscval  49267  cotval  49268