Theorem neeq1d 3001

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 2735	. 2 ⊢ (𝜑 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
3	2	necon3bid 2986	1 ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2942

This theorem is referenced by:  neeq1  3004  eqnetrd  3009  inisegn0  6098  f12dfv  7271  f13dfv  7272  suppval1  8152  elsuppfng  8155  elsuppfn  8156  suppsnop  8163  ressuppss  8168  ressuppssdif  8170  tz7.49  8445  ereldm  8751  pw2f1olem  9076  marypha1lem  9428  wdomtr  9570  inf3lem2  9624  cantnflem1  9684  cantnf  9688  cplem2  9885  dfac9  10131  kmlem12  10156  infpssrlem4  10301  fin23lem14  10328  axcc2lem  10431  axcc3  10433  domtriomlem  10437  axdc2lem  10443  ac6c4  10476  zorn2lem6  10496  rpnnen1lem4  12964  rpnnen1lem5  12965  mptnn0fsuppr  13964  hashprg  14355  hashtpg  14446  prodfn0  15840  prodfrec  15841  prodfdiv  15842  ntrivcvgtail  15846  fproddiv  15905  fprodn0  15923  fproddivf  15931  dvdsle  16253  algcvg  16513  algcvga  16516  eucalgcvga  16523  rpdvds  16597  phibndlem  16703  dfphi2  16707  pcaddlem  16821  vdwmc  16911  iscatd2  17625  brcic  17745  cicer  17753  cat1lem  18046  cat1  18047  sgrp2nmndlem5  18810  symgextf1lem  19288  pmtrmvd  19324  frgpup3lem  19645  isirred  20233  isdrngrd  20391  isdrngrdOLD  20393  rrgsupp  20907  dsmmelbas  21294  dsmmacl  21296  frlmssuvc2  21350  mhpsclcl  21690  mhpmulcl  21692  elcls  22577  clsndisj  22579  elcls3  22587  neindisj2  22627  clslp  22652  cmpfi  22912  cmpfii  22913  dfconn2  22923  connsuba  22924  nconnsubb  22927  1stcelcls  22965  finlocfin  23024  locfincmp  23030  dissnlocfin  23033  locfindis  23034  ptclsg  23119  dfac14lem  23121  isfbas  23333  trfbas2  23347  isfil  23351  filss  23357  fbunfip  23373  fgval  23374  elfg  23375  isufil2  23412  ufileu  23423  filufint  23424  fmfnfm  23462  flimclslem  23488  fclsopni  23519  fclsnei  23523  fclsbas  23525  fclsrest  23528  fclscmp  23534  ufilcmp  23536  isfcf  23538  fcfnei  23539  fcfneii  23541  ptcmplem2  23557  cnextcn  23571  cnextfres1  23572  tsmsfbas  23632  iscusp  23804  cuspcvg  23806  lpbl  24012  prdsxmslem2  24038  restmetu  24079  qdensere  24286  lebnumlem3  24479  isphtpc  24510  iscmet  24801  cmetcvg  24802  equivcmet  24834  cmetcusp1  24870  cmetcusp  24871  rrxmvallem  24921  ovolicc2lem2  25035  ovolicc2lem5  25038  i1fres  25223  lhop1lem  25530  deg1ldg  25610  plyco0  25706  plyeq0lem  25724  coeeq2  25756  coe1termlem  25772  taylfval  25871  cxpeq0  26186  ftalem4  26580  ftalem5  26581  ftalem6  26582  isppw  26618  isnsqf  26639  sqff1o  26686  musum  26695  dchrelbas3  26741  dchrelbasd  26742  dchrelbas4  26746  dchrmulcl  26752  dchrn0  26753  dchrfi  26758  dchrptlem2  26768  dchrpt  26770  lgsne0  26838  lgsdchr  26858  2sqlem11  26932  nosupbnd2lem1  27218  ishlg  27884  uvtx01vtx  28685  pthdlem2lem  29055  2pthdlem1  29215  clwwlknclwwlkdif  29263  umgr2cwwkdifex  29349  3pthdlem1  29448  frgrregorufr  29609  numclwwlk2lem1lem  29626  numclwwlk2lem1  29660  numclwlk2lem2f  29661  numclwlk2lem2f1o  29663  nmorepnf  30052  nmoprepnf  31151  nmfnrepnf  31164  ressupprn  31943  disjdsct  31955  rmfsupp2  32418  isufd  32663  fedgmullem2  32746  locfinreflem  32851  sibfof  33370  signswch  33603  signstfvneq0  33614  derangenlem  34193  subfacp1lem3  34204  subfacp1lem5  34206  subfacp1lem6  34207  subfacp1  34208  iscvm  34281  cvmcov  34285  cvmcov2  34297  eldm3  34762  elima4  34778  neibastop1  35292  neibastop2lem  35293  neibastop2  35294  neibastop3  35295  neifg  35304  poimirlem17  36553  poimirlem18  36554  poimirlem20  36556  poimirlem21  36557  poimirlem22  36558  poimirlem23  36559  poimirlem27  36563  poimirlem28  36564  poimirlem30  36566  poimirlem31  36567  poimirlem32  36568  mblfinlem3  36575  itg2addnclem3  36589  sstotbnd2  36690  cntotbnd  36712  heibor1lem  36725  dmecd  37221  disjecxrn  37307  br1cosscnvxrn  37392  2llnm3N  38488  dalem4  38584  cdlemk28-3  39827  mapdh9a  40708  sticksstones1  41010  metakunt29  41061  fsuppind  41210  dffltz  41424  pellexlem3  41617  mncn0  41929  aaitgo  41952  gneispace0nelrn2  42940  cvgdvgrat  43120  binomcxplemnotnn0  43163  disjf1  43928  disjrnmpt2  43934  disjinfi  43939  fsumiunss  44339  islptre  44383  islpcn  44403  lptre2pt  44404  0ellimcdiv  44413  liminflelimsup  44540  stoweidlem28  44792  stoweidlem43  44807  dirkercncflem2  44868  fourierdlem46  44916  fourierdlem79  44949  elaa2lem  44997  elaa2  44998  sge0fodjrnlem  45180  sge0iunmpt  45182  nnfoctbdjlem  45219  meadjiunlem  45229  meadjiun  45230  ovn0ssdmfun  46585  nzerooringczr  47018  rmsupp0  47092  scmsuppss  47096  suppmptcfin  47103  linc1  47154  el0ldep  47195  ldepspr  47202  islindeps2  47212  zlmodzxzldeplem4  47232  zlmodzxzldep  47233  ldepsnlinclem1  47234  ldepsnlinclem2  47235  ldepsnlinc  47237  fvconstr  47570  fvconstrn0  47571  fvconstr2  47572  catprslem  47678  catprsc  47681  catprsc2  47682  secval  47840  cscval  47841  cotval  47842