Theorem neeq1d 3015

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ≠ wne 2956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ne 2957

This theorem is referenced by:  neeq1  3018  eqnetrd  3023  iftrueb  4492  inisegn0  6084  f1ounsn  7252  f12dfv  7253  f13dfv  7254  resf1extb  7911  suppval1  8141  elsuppfng  8144  elsuppfn  8145  suppsnop  8153  ressuppss  8158  ressuppssdif  8160  tz7.49  8411  ereldm  8727  pw2f1olem  9049  marypha1lem  9376  wdomtr  9520  inf3lem2  9581  cantnflem1  9641  cantnf  9645  cplem2  9845  dfac9  10090  kmlem12  10115  infpssrlem4  10260  fin23lem14  10287  axcc2lem  10390  axcc3  10392  domtriomlem  10396  axdc2lem  10402  ac6c4  10435  zorn2lem6  10455  rpnnen1lem4  12978  rpnnen1lem5  12979  mptnn0fsuppr  14009  hashprg  14405  hashtpg  14495  prodfn0  15907  prodfrec  15908  prodfdiv  15909  ntrivcvgtail  15913  fproddiv  15974  fprodn0  15992  fproddivf  16000  dvdsle  16327  algcvg  16593  algcvga  16596  eucalgcvga  16603  rpdvds  16677  phibndlem  16788  dfphi2  16792  pcaddlem  16907  vdwmc  16997  iscatd2  17696  brcic  17814  cicer  17822  cat1lem  18112  cat1  18113  sgrp2nmndlem5  18949  symgextf1lem  19443  pmtrmvd  19479  frgpup3lem  19800  isirred  20447  rrgsupp  20730  isdrngrd  20795  isdrngrdOLD  20797  nzerooringczr  21512  dsmmelbas  21771  dsmmacl  21773  frlmssuvc2  21827  mhpsclcl  22192  mhpmulcl  22194  elcls  23113  clsndisj  23115  elcls3  23123  neindisj2  23163  clslp  23188  cmpfi  23448  cmpfii  23449  dfconn2  23459  connsuba  23460  nconnsubb  23463  1stcelcls  23501  finlocfin  23560  locfincmp  23566  dissnlocfin  23569  locfindis  23570  ptclsg  23655  dfac14lem  23657  isfbas  23869  trfbas2  23883  isfil  23887  filss  23893  fbunfip  23909  fgval  23910  elfg  23911  isufil2  23948  ufileu  23959  filufint  23960  fmfnfm  23998  flimclslem  24024  fclsopni  24055  fclsnei  24059  fclsbas  24061  fclsrest  24064  fclscmp  24070  ufilcmp  24072  isfcf  24074  fcfnei  24075  fcfneii  24077  ptcmplem2  24093  cnextcn  24107  cnextfres1  24108  tsmsfbas  24168  iscusp  24338  cuspcvg  24340  lpbl  24543  prdsxmslem2  24569  restmetu  24610  qdensere  24809  lebnumlem3  25005  isphtpc  25036  iscmet  25326  cmetcvg  25327  equivcmet  25359  cmetcusp1  25395  cmetcusp  25396  rrxmvallem  25446  ovolicc2lem2  25560  ovolicc2lem5  25563  i1fres  25747  lhop1lem  26055  deg1ldg  26132  plyco0  26232  plyeq0lem  26250  coeeq2  26282  coe1termlem  26298  taylfval  26399  cxpeq0  26720  ftalem4  27117  ftalem5  27118  ftalem6  27119  isppw  27155  isnsqf  27176  sqff1o  27223  musum  27232  dchrelbas3  27279  dchrelbasd  27280  dchrelbas4  27284  dchrmulcl  27290  dchrn0  27291  dchrfi  27296  dchrptlem2  27306  dchrpt  27308  lgsne0  27376  lgsdchr  27396  2sqlem11  27470  nosupbnd2lem1  27756  expsne0  28506  ishlg  28748  uvtx01vtx  29544  pthdlem2lem  29913  2pthdlem1  30076  clwwlknclwwlkdif  30127  umgr2cwwkdifex  30213  3pthdlem1  30312  frgrregorufr  30473  numclwwlk2lem1lem  30490  numclwwlk2lem1  30524  numclwlk2lem2f  30525  numclwlk2lem2f1o  30527  nmorepnf  30917  nmoprepnf  32016  nmfnrepnf  32029  fdifsupp  32837  ressupprn  32842  disjdsct  32855  suppgsumssiun  33213  rmfsupp2  33379  domnprodn0  33420  isufd  33697  ufdprmidl  33698  1arithufdlem4  33704  dfufd2lem  33706  fedgmullem2  33888  constrconj  34003  constrelextdg2  34005  constrllcllem  34010  constrcbvlem  34013  locfinreflem  34098  sibfof  34598  signswch  34819  signstfvneq0  34830  vonf1wev  35415  vonf1owevOLD  35417  derangenlem  35485  subfacp1lem3  35496  subfacp1lem5  35498  subfacp1lem6  35499  subfacp1  35500  iscvm  35573  cvmcov  35577  cvmcov2  35589  eldm3  36075  elima4  36090  neibastop1  36683  neibastop2lem  36684  neibastop2  36685  neibastop3  36686  neifg  36695  dfttc4lem1  36852  dfttc4lem2  36853  poimirlem17  38100  poimirlem18  38101  poimirlem20  38103  poimirlem21  38104  poimirlem22  38105  poimirlem23  38106  poimirlem27  38110  poimirlem28  38111  poimirlem30  38113  poimirlem31  38114  poimirlem32  38115  mblfinlem3  38122  itg2addnclem3  38136  sstotbnd2  38237  cntotbnd  38259  heibor1lem  38272  dmecd  38773  disjecxrn  38875  br1cosscnvxrn  39027  disjimeceqim  39267  eldisjim3  39278  2llnm3N  40157  dalem4  40253  cdlemk28-3  41496  mapdh9a  42377  idomnnzpownz  42713  idomnnzgmulnz  42714  sticksstones1  42727  aks6d1c6lem1  42751  unitscyglem2  42777  unitscyglem3  42778  unitscyglem4  42779  readvcot  42937  domnexpgn0cl  43105  fsuppind  43136  dffltz  43180  pellexlem3  43372  mncn0  43680  aaitgo  43703  gneispace0nelrn2  44681  cvgdvgrat  44853  binomcxplemnotnn0  44896  disjf1  45725  disjrnmpt2  45730  disjinfi  45734  fsumiunss  46115  islptre  46159  islpcn  46177  lptre2pt  46178  0ellimcdiv  46187  liminflelimsup  46314  stoweidlem28  46566  stoweidlem43  46581  dirkercncflem2  46642  fourierdlem46  46690  fourierdlem79  46723  elaa2lem  46771  elaa2  46772  sge0fodjrnlem  46954  sge0iunmpt  46956  nnfoctbdjlem  46993  meadjiunlem  47003  meadjiun  47004  gpg5nbgrvtx13starlem1  48657  gpg5nbgrvtx13starlem3  48659  ovn0ssdmfun  48745  rmsupp0  48954  scmsuppss  48957  suppmptcfin  48962  linc1  49011  el0ldep  49052  ldepspr  49059  islindeps2  49069  zlmodzxzldeplem4  49089  zlmodzxzldep  49090  ldepsnlinclem1  49091  ldepsnlinclem2  49092  ldepsnlinc  49094  fvconstr  49447  fvconstrn0  49448  fvconstr2  49449  catprslem  49595  catprsc  49598  catprsc2  49599  oppccic  49629  relcic  49630  cicpropdlem  49634  secval  50332  cscval  50333  cotval  50334