Theorem neeq1d 3018

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  neeq1  3021  eqnetrd  3026  iftrueb  4498  inisegn0  6109  f1ounsn  7306  f12dfv  7307  f13dfv  7308  ovn0ssdmfun  7616  resf1extb  7973  suppval1  8214  elsuppfng  8217  elsuppfn  8218  suppsnop  8226  ressuppss  8231  ressuppssdif  8233  tz7.49  8486  ereldm  8802  pw2f1olem  9131  marypha1lem  9455  wdomtr  9599  inf3lem2  9660  cantnflem1  9720  cantnf  9724  cplem2  9982  cplem2OLD  9983  dfac9  10245  kmlem12  10270  infpssrlem4  10414  fin23lem14  10441  axcc2lem  10544  axcc3  10546  domtriomlem  10550  axdc2lem  10556  ac6c4  10589  zorn2lem6  10609  rpnnen1lem4  13138  rpnnen1lem5  13139  mptnn0fsuppr  14172  hashprg  14569  hashtpg  14660  prodfn0  16095  prodfrec  16096  prodfdiv  16097  ntrivcvgtail  16101  fproddiv  16160  fprodn0  16178  fproddivf  16186  dvdsle  16512  algcvg  16783  algcvga  16786  eucalgcvga  16793  rpdvds  16867  phibndlem  16979  dfphi2  16983  pcaddlem  17098  vdwmc  17188  iscatd2  17887  brcic  18005  cicer  18013  cat1lem  18303  cat1  18304  sgrp2nmndlem5  19160  symgextf1lem  19667  pmtrmvd  19703  frgpup3lem  20024  isirred  20682  rrgsupp  20986  isdrngrd  21056  isdrngrdOLD  21058  nzerooringczr  21819  dsmmelbas  22078  dsmmacl  22080  frlmssuvc2  22134  mhpsclcl  22501  mhpmulcl  22503  elcls  23424  clsndisj  23426  elcls3  23434  neindisj2  23474  clslp  23499  cmpfi  23759  cmpfii  23760  dfconn2  23770  connsuba  23771  nconnsubb  23774  1stcelcls  23813  finlocfin  23872  locfincmp  23878  dissnlocfin  23881  locfindis  23882  ptclsg  23967  dfac14lem  23969  isfbas  24181  trfbas2  24195  isfil  24199  filss  24205  fbunfip  24221  fgval  24222  elfg  24223  isufil2  24260  ufileu  24271  filufint  24272  fmfnfm  24310  flimclslem  24336  fclsopni  24367  fclsnei  24371  fclsbas  24373  fclsrest  24376  fclscmp  24382  ufilcmp  24384  isfcf  24386  fcfnei  24387  fcfneii  24389  ptcmplem2  24405  cnextcn  24419  cnextfres1  24420  tsmsfbas  24480  iscusp  24650  cuspcvg  24652  lpbl  24855  prdsxmslem2  24881  restmetu  24922  qdensere  25121  lebnumlem3  25317  isphtpc  25348  iscmet  25638  cmetcvg  25639  equivcmet  25671  cmetcusp1  25707  cmetcusp  25708  rrxmvallem  25758  ovolicc2lem2  25872  ovolicc2lem5  25875  i1fres  26059  lhop1lem  26366  deg1ldg  26443  plyco0  26543  plyeq0lem  26562  coeeq2  26594  coe1termlem  26610  rnplynfin  26663  plyconz  26664  taylfval  26719  cxpeq0  27039  ftalem4  27436  ftalem5  27437  ftalem6  27438  isppw  27474  isnsqf  27495  sqff1o  27542  musum  27551  dchrelbas3  27598  dchrelbasd  27599  dchrelbas4  27603  dchrmulcl  27609  dchrn0  27610  dchrfi  27615  dchrptlem2  27625  dchrpt  27627  lgsne0  27695  lgsdchr  27715  2sqlem11  27789  flt4ALT  28025  fltoprm  28028  nosupbnd2lem1  28105  expsne0  28855  ishlg2  29098  ishlg  29101  elcgrabasi  29408  angmgmaddov1  29421  angmgmaddcpbl  29423  angmgmaddcl  29424  angmgmval  29427  uvtx01vtx  30011  pthdlem2lem  30386  2pthdlem1  30552  clwwlknclwwlkdif  30603  umgr2cwwkdifex  30689  3pthdlem1  30798  frgrregorufr  30959  numclwwlk2lem1lem  30976  numclwwlk2lem1  31010  numclwlk2lem2f  31011  numclwlk2lem2f1o  31013  nmorepnf  31403  nmoprepnf  32502  nmfnrepnf  32515  fdifsupp  33352  ressupprn  33357  disjdsct  33370  suppgsumssiun  33709  rmfsupp2  33874  domnprodn0  33915  isufd  34156  ufdprmidl  34157  1arithufdlem4  34163  dfufd2lem  34165  fedgmullem2  34345  constrconj  34460  constrelextdg2  34462  constrllcllem  34467  constrcbvlem  34470  locfinreflem  34555  sibfof  35055  signswch  35273  signstfvneq0  35284  vonf1wev  36049  vonf1owevOLD  36051  derangenlem  36116  subfacp1lem3  36127  subfacp1lem5  36129  subfacp1lem6  36130  subfacp1  36131  iscvm  36204  cvmcov  36208  cvmcov2  36220  eldm3  36717  elima4  36731  neibastop1  37338  neibastop2lem  37339  neibastop2  37340  neibastop3  37341  neifg  37350  dfttc4lem1  37507  dfttc4lem2  37508  mh-inf3f1  37520  poimirlem17  38760  poimirlem18  38761  poimirlem20  38763  poimirlem21  38764  poimirlem22  38765  poimirlem23  38766  poimirlem27  38770  poimirlem28  38771  poimirlem30  38773  poimirlem31  38774  poimirlem32  38775  mblfinlem3  38782  itg2addnclem3  38796  sstotbnd2  38911  cntotbnd  38933  heibor1lem  38946  dmecd  39445  disjecxrn  39547  br1cosscnvxrn  39699  disjimeceqim  39939  eldisjim3  39950  2llnm3N  40829  dalem4  40925  cdlemk28-3  42168  mapdh9a  43049  idomnnzpownz  43385  idomnnzgmulnz  43386  sticksstones1  43399  aks6d1c6lem1  43423  unitscyglem2  43449  unitscyglem3  43450  unitscyglem4  43451  readvcot  43619  domnexpgn0cl  43788  fsuppind  43822  frlmnzcoordval  43857  frlmnzcoordn0  43861  dffltz  43874  pellexlem3  44042  mncn0  44344  aaitgo  44367  gneispace0nelrn2  45344  cvgdvgrat  45500  binomcxplemnotnn0  45543  disjf1  46413  disjrnmpt2  46418  disjinfi  46422  fsumiunss  46802  islptre  46846  islpcn  46864  lptre2pt  46865  0ellimcdiv  46874  liminflelimsup  47001  stoweidlem28  47253  stoweidlem43  47268  dirkercncflem2  47329  fourierdlem46  47377  fourierdlem79  47410  elaa2lem  47458  elaa2  47459  sge0fodjrnlem  47641  sge0iunmpt  47643  nnfoctbdjlem  47680  meadjiunlem  47690  meadjiun  47691  gpg5nbgrvtx13starlem1  49384  gpg5nbgrvtx13starlem3  49386  rmsupp0  49695  scmsuppss  49698  suppmptcfin  49703  linc1  49752  el0ldep  49793  ldepspr  49800  islindeps2  49810  zlmodzxzldeplem4  49830  zlmodzxzldep  49831  ldepsnlinclem1  49832  ldepsnlinclem2  49833  ldepsnlinc  49835  ovconstbrd  50188  ovconstbrn0d  50189  elovconstbrd  50190  catprslem  50339  catprsc  50342  catprsc2  50343  oppccic  50373  relcic  50374  cicpropdlem  50378  secval  51152  cscval  51153  cotval  51154  dvsec  51168  dvcsc  51169  dvcot  51170