Theorem neeq1d 3020

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

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

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

This theorem is used by:  neeq1  3023  eqnetrd  3028  iftrueb  4505  inisegn0  6105  f1ounsn  7281  f12dfv  7282  f13dfv  7283  resf1extb  7940  suppval1  8171  elsuppfng  8174  elsuppfn  8175  suppsnop  8183  ressuppss  8188  ressuppssdif  8190  tz7.49  8441  ereldm  8757  pw2f1olem  9079  marypha1lem  9403  wdomtr  9547  inf3lem2  9608  cantnflem1  9668  cantnf  9672  cplem2  9891  cplem2OLD  9892  dfac9  10139  kmlem12  10164  infpssrlem4  10308  fin23lem14  10335  axcc2lem  10438  axcc3  10440  domtriomlem  10444  axdc2lem  10450  ac6c4  10483  zorn2lem6  10503  rpnnen1lem4  13022  rpnnen1lem5  13023  mptnn0fsuppr  14055  hashprg  14451  hashtpg  14542  prodfn0  15974  prodfrec  15975  prodfdiv  15976  ntrivcvgtail  15980  fproddiv  16041  fprodn0  16059  fproddivf  16067  dvdsle  16393  algcvg  16659  algcvga  16662  eucalgcvga  16669  rpdvds  16743  phibndlem  16854  dfphi2  16858  pcaddlem  16973  vdwmc  17063  iscatd2  17762  brcic  17880  cicer  17888  cat1lem  18178  cat1  18179  sgrp2nmndlem5  19022  symgextf1lem  19521  pmtrmvd  19557  frgpup3lem  19878  isirred  20534  rrgsupp  20837  isdrngrd  20906  isdrngrdOLD  20908  nzerooringczr  21667  dsmmelbas  21926  dsmmacl  21928  frlmssuvc2  21982  mhpsclcl  22347  mhpmulcl  22349  elcls  23267  clsndisj  23269  elcls3  23277  neindisj2  23317  clslp  23342  cmpfi  23602  cmpfii  23603  dfconn2  23613  connsuba  23614  nconnsubb  23617  1stcelcls  23655  finlocfin  23714  locfincmp  23720  dissnlocfin  23723  locfindis  23724  ptclsg  23809  dfac14lem  23811  isfbas  24023  trfbas2  24037  isfil  24041  filss  24047  fbunfip  24063  fgval  24064  elfg  24065  isufil2  24102  ufileu  24113  filufint  24114  fmfnfm  24152  flimclslem  24178  fclsopni  24209  fclsnei  24213  fclsbas  24215  fclsrest  24218  fclscmp  24224  ufilcmp  24226  isfcf  24228  fcfnei  24229  fcfneii  24231  ptcmplem2  24247  cnextcn  24261  cnextfres1  24262  tsmsfbas  24322  iscusp  24492  cuspcvg  24494  lpbl  24697  prdsxmslem2  24723  restmetu  24764  qdensere  24963  lebnumlem3  25159  isphtpc  25190  iscmet  25480  cmetcvg  25481  equivcmet  25513  cmetcusp1  25549  cmetcusp  25550  rrxmvallem  25600  ovolicc2lem2  25714  ovolicc2lem5  25717  i1fres  25901  lhop1lem  26209  deg1ldg  26286  plyco0  26386  plyeq0lem  26404  coeeq2  26436  coe1termlem  26452  taylfval  26559  cxpeq0  26880  ftalem4  27277  ftalem5  27278  ftalem6  27279  isppw  27315  isnsqf  27336  sqff1o  27383  musum  27392  dchrelbas3  27439  dchrelbasd  27440  dchrelbas4  27444  dchrmulcl  27450  dchrn0  27451  dchrfi  27456  dchrptlem2  27466  dchrpt  27468  lgsne0  27536  lgsdchr  27556  2sqlem11  27630  nosupbnd2lem1  27916  expsne0  28666  ishlg2  28908  ishlg  28911  uvtx01vtx  29784  pthdlem2lem  30153  2pthdlem1  30316  clwwlknclwwlkdif  30367  umgr2cwwkdifex  30453  3pthdlem1  30552  frgrregorufr  30713  numclwwlk2lem1lem  30730  numclwwlk2lem1  30764  numclwlk2lem2f  30765  numclwlk2lem2f1o  30767  nmorepnf  31157  nmoprepnf  32256  nmfnrepnf  32269  fdifsupp  33067  ressupprn  33072  disjdsct  33085  suppgsumssiun  33423  rmfsupp2  33588  domnprodn0  33629  isufd  33861  ufdprmidl  33862  1arithufdlem4  33868  dfufd2lem  33870  fedgmullem2  34051  constrconj  34166  constrelextdg2  34168  constrllcllem  34173  constrcbvlem  34176  locfinreflem  34261  sibfof  34762  signswch  34980  signstfvneq0  34991  vonf1wev  35616  vonf1owevOLD  35618  derangenlem  35684  subfacp1lem3  35695  subfacp1lem5  35697  subfacp1lem6  35698  subfacp1  35699  iscvm  35772  cvmcov  35776  cvmcov2  35788  eldm3  36274  elima4  36289  neibastop1  36911  neibastop2lem  36912  neibastop2  36913  neibastop3  36914  neifg  36923  dfttc4lem1  37080  dfttc4lem2  37081  poimirlem17  38329  poimirlem18  38330  poimirlem20  38332  poimirlem21  38333  poimirlem22  38334  poimirlem23  38335  poimirlem27  38339  poimirlem28  38340  poimirlem30  38342  poimirlem31  38343  poimirlem32  38344  mblfinlem3  38351  itg2addnclem3  38365  sstotbnd2  38466  cntotbnd  38488  heibor1lem  38501  dmecd  39000  disjecxrn  39102  br1cosscnvxrn  39254  disjimeceqim  39494  eldisjim3  39505  2llnm3N  40384  dalem4  40480  cdlemk28-3  41723  mapdh9a  42604  idomnnzpownz  42940  idomnnzgmulnz  42941  sticksstones1  42954  aks6d1c6lem1  42978  unitscyglem2  43004  unitscyglem3  43005  unitscyglem4  43006  readvcot  43166  domnexpgn0cl  43332  fsuppind  43363  dffltz  43407  pellexlem3  43599  mncn0  43907  aaitgo  43930  gneispace0nelrn2  44908  cvgdvgrat  45064  binomcxplemnotnn0  45107  disjf1  45942  disjrnmpt2  45947  disjinfi  45951  fsumiunss  46332  islptre  46376  islpcn  46394  lptre2pt  46395  0ellimcdiv  46404  liminflelimsup  46531  stoweidlem28  46783  stoweidlem43  46798  dirkercncflem2  46859  fourierdlem46  46907  fourierdlem79  46940  elaa2lem  46988  elaa2  46989  sge0fodjrnlem  47171  sge0iunmpt  47173  nnfoctbdjlem  47210  meadjiunlem  47220  meadjiun  47221  gpg5nbgrvtx13starlem1  48877  gpg5nbgrvtx13starlem3  48879  ovn0ssdmfun  48965  rmsupp0  49189  scmsuppss  49192  suppmptcfin  49197  linc1  49246  el0ldep  49287  ldepspr  49294  islindeps2  49304  zlmodzxzldeplem4  49324  zlmodzxzldep  49325  ldepsnlinclem1  49326  ldepsnlinclem2  49327  ldepsnlinc  49329  fvconstr  49681  fvconstrn0  49682  fvconstr2  49683  catprslem  49829  catprsc  49832  catprsc2  49833  oppccic  49863  relcic  49864  cicpropdlem  49868  secval  50566  cscval  50567  cotval  50568