Theorem neeq1d 3016

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

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

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 2155  ax-ext 2734

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

This theorem is used by:  neeq1  3019  eqnetrd  3024  iftrueb  4498  inisegn0  6098  f1ounsn  7277  f12dfv  7278  f13dfv  7279  ovn0ssdmfun  7586  resf1extb  7935  suppval1  8168  elsuppfng  8171  elsuppfn  8172  suppsnop  8180  ressuppss  8185  ressuppssdif  8187  tz7.49  8438  ereldm  8754  pw2f1olem  9083  marypha1lem  9407  wdomtr  9551  inf3lem2  9612  cantnflem1  9672  cantnf  9676  cplem2  9895  cplem2OLD  9896  dfac9  10143  kmlem12  10168  infpssrlem4  10312  fin23lem14  10339  axcc2lem  10442  axcc3  10444  domtriomlem  10448  axdc2lem  10454  ac6c4  10487  zorn2lem6  10507  rpnnen1lem4  13034  rpnnen1lem5  13035  mptnn0fsuppr  14067  hashprg  14463  hashtpg  14554  prodfn0  15987  prodfrec  15988  prodfdiv  15989  ntrivcvgtail  15993  fproddiv  16054  fprodn0  16072  fproddivf  16080  dvdsle  16406  algcvg  16672  algcvga  16675  eucalgcvga  16682  rpdvds  16756  phibndlem  16867  dfphi2  16871  pcaddlem  16986  vdwmc  17076  iscatd2  17775  brcic  17893  cicer  17901  cat1lem  18191  cat1  18192  sgrp2nmndlem5  19047  symgextf1lem  19553  pmtrmvd  19589  frgpup3lem  19910  isirred  20566  rrgsupp  20869  isdrngrd  20938  isdrngrdOLD  20940  nzerooringczr  21699  dsmmelbas  21958  dsmmacl  21960  frlmssuvc2  22014  mhpsclcl  22381  mhpmulcl  22383  elcls  23304  clsndisj  23306  elcls3  23314  neindisj2  23354  clslp  23379  cmpfi  23639  cmpfii  23640  dfconn2  23650  connsuba  23651  nconnsubb  23654  1stcelcls  23693  finlocfin  23752  locfincmp  23758  dissnlocfin  23761  locfindis  23762  ptclsg  23847  dfac14lem  23849  isfbas  24061  trfbas2  24075  isfil  24079  filss  24085  fbunfip  24101  fgval  24102  elfg  24103  isufil2  24140  ufileu  24151  filufint  24152  fmfnfm  24190  flimclslem  24216  fclsopni  24247  fclsnei  24251  fclsbas  24253  fclsrest  24256  fclscmp  24262  ufilcmp  24264  isfcf  24266  fcfnei  24267  fcfneii  24269  ptcmplem2  24285  cnextcn  24299  cnextfres1  24300  tsmsfbas  24360  iscusp  24530  cuspcvg  24532  lpbl  24735  prdsxmslem2  24761  restmetu  24802  qdensere  25001  lebnumlem3  25197  isphtpc  25228  iscmet  25518  cmetcvg  25519  equivcmet  25551  cmetcusp1  25587  cmetcusp  25588  rrxmvallem  25638  ovolicc2lem2  25752  ovolicc2lem5  25755  i1fres  25939  lhop1lem  26247  deg1ldg  26324  plyco0  26424  plyeq0lem  26443  coeeq2  26475  coe1termlem  26491  rnplynfin  26546  plyconz  26547  taylfval  26602  cxpeq0  26923  ftalem4  27320  ftalem5  27321  ftalem6  27322  isppw  27358  isnsqf  27379  sqff1o  27426  musum  27435  dchrelbas3  27482  dchrelbasd  27483  dchrelbas4  27487  dchrmulcl  27493  dchrn0  27494  dchrfi  27499  dchrptlem2  27509  dchrpt  27511  lgsne0  27579  lgsdchr  27599  2sqlem11  27673  nosupbnd2lem1  27959  expsne0  28709  ishlg2  28952  ishlg  28955  elcgrabasi  29262  angmgmaddov1  29275  angmgmaddcpbl  29277  angmgmaddcl  29278  angmgmval  29281  uvtx01vtx  29865  pthdlem2lem  30240  2pthdlem1  30406  clwwlknclwwlkdif  30457  umgr2cwwkdifex  30543  3pthdlem1  30652  frgrregorufr  30813  numclwwlk2lem1lem  30830  numclwwlk2lem1  30864  numclwlk2lem2f  30865  numclwlk2lem2f1o  30867  nmorepnf  31257  nmoprepnf  32356  nmfnrepnf  32369  fdifsupp  33165  ressupprn  33170  disjdsct  33183  suppgsumssiun  33520  rmfsupp2  33685  domnprodn0  33726  isufd  33958  ufdprmidl  33959  1arithufdlem4  33965  dfufd2lem  33967  fedgmullem2  34148  constrconj  34263  constrelextdg2  34265  constrllcllem  34270  constrcbvlem  34273  locfinreflem  34358  sibfof  34859  signswch  35077  signstfvneq0  35088  vonf1wev  35713  vonf1owevOLD  35715  derangenlem  35758  subfacp1lem3  35769  subfacp1lem5  35771  subfacp1lem6  35772  subfacp1  35773  iscvm  35846  cvmcov  35850  cvmcov2  35862  eldm3  36348  elima4  36363  neibastop1  36986  neibastop2lem  36987  neibastop2  36988  neibastop3  36989  neifg  36998  dfttc4lem1  37155  dfttc4lem2  37156  poimirlem17  38394  poimirlem18  38395  poimirlem20  38397  poimirlem21  38398  poimirlem22  38399  poimirlem23  38400  poimirlem27  38404  poimirlem28  38405  poimirlem30  38407  poimirlem31  38408  poimirlem32  38409  mblfinlem3  38416  itg2addnclem3  38430  sstotbnd2  38532  cntotbnd  38554  heibor1lem  38567  dmecd  39066  disjecxrn  39168  br1cosscnvxrn  39320  disjimeceqim  39560  eldisjim3  39571  2llnm3N  40450  dalem4  40546  cdlemk28-3  41789  mapdh9a  42670  idomnnzpownz  43006  idomnnzgmulnz  43007  sticksstones1  43020  aks6d1c6lem1  43044  unitscyglem2  43070  unitscyglem3  43071  unitscyglem4  43072  readvcot  43247  domnexpgn0cl  43413  fsuppind  43444  dffltz  43488  pellexlem3  43680  mncn0  43988  aaitgo  44011  gneispace0nelrn2  44989  cvgdvgrat  45145  binomcxplemnotnn0  45188  disjf1  46023  disjrnmpt2  46028  disjinfi  46032  fsumiunss  46413  islptre  46457  islpcn  46475  lptre2pt  46476  0ellimcdiv  46485  liminflelimsup  46612  stoweidlem28  46864  stoweidlem43  46879  dirkercncflem2  46940  fourierdlem46  46988  fourierdlem79  47021  elaa2lem  47069  elaa2  47070  sge0fodjrnlem  47252  sge0iunmpt  47254  nnfoctbdjlem  47291  meadjiunlem  47301  meadjiun  47302  gpg5nbgrvtx13starlem1  48995  gpg5nbgrvtx13starlem3  48997  rmsupp0  49306  scmsuppss  49309  suppmptcfin  49314  linc1  49363  el0ldep  49404  ldepspr  49411  islindeps2  49421  zlmodzxzldeplem4  49441  zlmodzxzldep  49442  ldepsnlinclem1  49443  ldepsnlinclem2  49444  ldepsnlinc  49446  fvconstr  49798  fvconstrn0  49799  fvconstr2  49800  catprslem  49944  catprsc  49947  catprsc2  49948  oppccic  49978  relcic  49979  cicpropdlem  49983  secval  50681  cscval  50682  cotval  50683  dvsec  50697  dvcsc  50698  dvcot  50699