Theorem neeq1d 2992

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  neeq1  2995  eqnetrd  3000  iftrueb  4480  inisegn0  6057  f1ounsn  7220  f12dfv  7221  f13dfv  7222  resf1extb  7878  suppval1  8109  elsuppfng  8112  elsuppfn  8113  suppsnop  8121  ressuppss  8126  ressuppssdif  8128  tz7.49  8377  ereldm  8690  pw2f1olem  9012  marypha1lem  9339  wdomtr  9483  inf3lem2  9541  cantnflem1  9601  cantnf  9605  cplem2  9805  dfac9  10050  kmlem12  10075  infpssrlem4  10219  fin23lem14  10246  axcc2lem  10349  axcc3  10351  domtriomlem  10355  axdc2lem  10361  ac6c4  10394  zorn2lem6  10414  rpnnen1lem4  12921  rpnnen1lem5  12922  mptnn0fsuppr  13952  hashprg  14348  hashtpg  14438  prodfn0  15850  prodfrec  15851  prodfdiv  15852  ntrivcvgtail  15856  fproddiv  15917  fprodn0  15935  fproddivf  15943  dvdsle  16270  algcvg  16536  algcvga  16539  eucalgcvga  16546  rpdvds  16620  phibndlem  16731  dfphi2  16735  pcaddlem  16850  vdwmc  16940  iscatd2  17638  brcic  17756  cicer  17764  cat1lem  18054  cat1  18055  sgrp2nmndlem5  18891  symgextf1lem  19386  pmtrmvd  19422  frgpup3lem  19743  isirred  20390  rrgsupp  20669  isdrngrd  20734  isdrngrdOLD  20736  nzerooringczr  21470  dsmmelbas  21729  dsmmacl  21731  frlmssuvc2  21785  mhpsclcl  22123  mhpmulcl  22125  elcls  23048  clsndisj  23050  elcls3  23058  neindisj2  23098  clslp  23123  cmpfi  23383  cmpfii  23384  dfconn2  23394  connsuba  23395  nconnsubb  23398  1stcelcls  23436  finlocfin  23495  locfincmp  23501  dissnlocfin  23504  locfindis  23505  ptclsg  23590  dfac14lem  23592  isfbas  23804  trfbas2  23818  isfil  23822  filss  23828  fbunfip  23844  fgval  23845  elfg  23846  isufil2  23883  ufileu  23894  filufint  23895  fmfnfm  23933  flimclslem  23959  fclsopni  23990  fclsnei  23994  fclsbas  23996  fclsrest  23999  fclscmp  24005  ufilcmp  24007  isfcf  24009  fcfnei  24010  fcfneii  24012  ptcmplem2  24028  cnextcn  24042  cnextfres1  24043  tsmsfbas  24103  iscusp  24273  cuspcvg  24275  lpbl  24478  prdsxmslem2  24504  restmetu  24545  qdensere  24744  lebnumlem3  24940  isphtpc  24971  iscmet  25261  cmetcvg  25262  equivcmet  25294  cmetcusp1  25330  cmetcusp  25331  rrxmvallem  25381  ovolicc2lem2  25495  ovolicc2lem5  25498  i1fres  25682  lhop1lem  25990  deg1ldg  26067  plyco0  26167  plyeq0lem  26185  coeeq2  26217  coe1termlem  26233  taylfval  26335  cxpeq0  26655  ftalem4  27053  ftalem5  27054  ftalem6  27055  isppw  27091  isnsqf  27112  sqff1o  27159  musum  27168  dchrelbas3  27215  dchrelbasd  27216  dchrelbas4  27220  dchrmulcl  27226  dchrn0  27227  dchrfi  27232  dchrptlem2  27242  dchrpt  27244  lgsne0  27312  lgsdchr  27332  2sqlem11  27406  nosupbnd2lem1  27693  expsne0  28442  ishlg  28684  uvtx01vtx  29480  pthdlem2lem  29850  2pthdlem1  30013  clwwlknclwwlkdif  30064  umgr2cwwkdifex  30150  3pthdlem1  30249  frgrregorufr  30410  numclwwlk2lem1lem  30427  numclwwlk2lem1  30461  numclwlk2lem2f  30462  numclwlk2lem2f1o  30464  nmorepnf  30854  nmoprepnf  31953  nmfnrepnf  31966  fdifsupp  32773  ressupprn  32778  disjdsct  32791  suppgsumssiun  33148  rmfsupp2  33314  domnprodn0  33351  isufd  33615  ufdprmidl  33616  1arithufdlem4  33622  dfufd2lem  33624  fedgmullem2  33790  constrconj  33905  constrelextdg2  33907  constrllcllem  33912  constrcbvlem  33915  locfinreflem  34000  sibfof  34500  signswch  34721  signstfvneq0  34732  vonf1owev  35306  derangenlem  35369  subfacp1lem3  35380  subfacp1lem5  35382  subfacp1lem6  35383  subfacp1  35384  iscvm  35457  cvmcov  35461  cvmcov2  35473  eldm3  35959  elima4  35974  neibastop1  36557  neibastop2lem  36558  neibastop2  36559  neibastop3  36560  neifg  36569  dfttc4lem1  36726  dfttc4lem2  36727  poimirlem17  37972  poimirlem18  37973  poimirlem20  37975  poimirlem21  37976  poimirlem22  37977  poimirlem23  37978  poimirlem27  37982  poimirlem28  37983  poimirlem30  37985  poimirlem31  37986  poimirlem32  37987  mblfinlem3  37994  itg2addnclem3  38008  sstotbnd2  38109  cntotbnd  38131  heibor1lem  38144  dmecd  38645  disjecxrn  38747  br1cosscnvxrn  38899  disjimeceqim  39139  eldisjim3  39150  2llnm3N  40029  dalem4  40125  cdlemk28-3  41368  mapdh9a  42249  idomnnzpownz  42585  idomnnzgmulnz  42586  sticksstones1  42599  aks6d1c6lem1  42623  unitscyglem2  42649  unitscyglem3  42650  unitscyglem4  42651  readvcot  42810  domnexpgn0cl  42982  fsuppind  43037  dffltz  43081  pellexlem3  43277  mncn0  43585  aaitgo  43608  gneispace0nelrn2  44586  cvgdvgrat  44758  binomcxplemnotnn0  44801  disjf1  45631  disjrnmpt2  45636  disjinfi  45640  fsumiunss  46023  islptre  46067  islpcn  46085  lptre2pt  46086  0ellimcdiv  46095  liminflelimsup  46222  stoweidlem28  46474  stoweidlem43  46489  dirkercncflem2  46550  fourierdlem46  46598  fourierdlem79  46631  elaa2lem  46679  elaa2  46680  sge0fodjrnlem  46862  sge0iunmpt  46864  nnfoctbdjlem  46901  meadjiunlem  46911  meadjiun  46912  gpg5nbgrvtx13starlem1  48559  gpg5nbgrvtx13starlem3  48561  ovn0ssdmfun  48647  rmsupp0  48856  scmsuppss  48859  suppmptcfin  48864  linc1  48913  el0ldep  48954  ldepspr  48961  islindeps2  48971  zlmodzxzldeplem4  48991  zlmodzxzldep  48992  ldepsnlinclem1  48993  ldepsnlinclem2  48994  ldepsnlinc  48996  fvconstr  49349  fvconstrn0  49350  fvconstr2  49351  catprslem  49497  catprsc  49500  catprsc2  49501  oppccic  49531  relcic  49532  cicpropdlem  49536  secval  50234  cscval  50235  cotval  50236