Theorem neeq1d 3017

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ≠ wne 2958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ne 2959

This theorem is referenced by:  neeq1  3020  eqnetrd  3025  iftrueb  4501  inisegn0  6102  f1ounsn  7272  f12dfv  7273  f13dfv  7274  resf1extb  7932  suppval1  8163  elsuppfng  8166  elsuppfn  8167  suppsnop  8175  ressuppss  8180  ressuppssdif  8182  tz7.49  8433  ereldm  8749  pw2f1olem  9070  marypha1lem  9394  wdomtr  9538  inf3lem2  9599  cantnflem1  9659  cantnf  9663  cplem2  9877  dfac9  10121  kmlem12  10146  infpssrlem4  10291  fin23lem14  10318  axcc2lem  10421  axcc3  10423  domtriomlem  10427  axdc2lem  10433  ac6c4  10466  zorn2lem6  10486  rpnnen1lem4  13005  rpnnen1lem5  13006  mptnn0fsuppr  14037  hashprg  14433  hashtpg  14524  prodfn0  15950  prodfrec  15951  prodfdiv  15952  ntrivcvgtail  15956  fproddiv  16017  fprodn0  16035  fproddivf  16043  dvdsle  16369  algcvg  16635  algcvga  16638  eucalgcvga  16645  rpdvds  16719  phibndlem  16830  dfphi2  16834  pcaddlem  16949  vdwmc  17039  iscatd2  17738  brcic  17856  cicer  17864  cat1lem  18154  cat1  18155  sgrp2nmndlem5  18992  symgextf1lem  19491  pmtrmvd  19527  frgpup3lem  19848  isirred  20502  rrgsupp  20787  isdrngrd  20851  isdrngrdOLD  20853  nzerooringczr  21611  dsmmelbas  21870  dsmmacl  21872  frlmssuvc2  21926  mhpsclcl  22291  mhpmulcl  22293  elcls  23211  clsndisj  23213  elcls3  23221  neindisj2  23261  clslp  23286  cmpfi  23546  cmpfii  23547  dfconn2  23557  connsuba  23558  nconnsubb  23561  1stcelcls  23599  finlocfin  23658  locfincmp  23664  dissnlocfin  23667  locfindis  23668  ptclsg  23753  dfac14lem  23755  isfbas  23967  trfbas2  23981  isfil  23985  filss  23991  fbunfip  24007  fgval  24008  elfg  24009  isufil2  24046  ufileu  24057  filufint  24058  fmfnfm  24096  flimclslem  24122  fclsopni  24153  fclsnei  24157  fclsbas  24159  fclsrest  24162  fclscmp  24168  ufilcmp  24170  isfcf  24172  fcfnei  24173  fcfneii  24175  ptcmplem2  24191  cnextcn  24205  cnextfres1  24206  tsmsfbas  24266  iscusp  24436  cuspcvg  24438  lpbl  24641  prdsxmslem2  24667  restmetu  24708  qdensere  24907  lebnumlem3  25103  isphtpc  25134  iscmet  25424  cmetcvg  25425  equivcmet  25457  cmetcusp1  25493  cmetcusp  25494  rrxmvallem  25544  ovolicc2lem2  25658  ovolicc2lem5  25661  i1fres  25845  lhop1lem  26153  deg1ldg  26230  plyco0  26330  plyeq0lem  26348  coeeq2  26380  coe1termlem  26396  taylfval  26500  cxpeq0  26821  ftalem4  27218  ftalem5  27219  ftalem6  27220  isppw  27256  isnsqf  27277  sqff1o  27324  musum  27333  dchrelbas3  27380  dchrelbasd  27381  dchrelbas4  27385  dchrmulcl  27391  dchrn0  27392  dchrfi  27397  dchrptlem2  27407  dchrpt  27409  lgsne0  27477  lgsdchr  27497  2sqlem11  27571  nosupbnd2lem1  27857  expsne0  28607  ishlg2  28849  ishlg  28852  uvtx01vtx  29725  pthdlem2lem  30094  2pthdlem1  30257  clwwlknclwwlkdif  30308  umgr2cwwkdifex  30394  3pthdlem1  30493  frgrregorufr  30654  numclwwlk2lem1lem  30671  numclwwlk2lem1  30705  numclwlk2lem2f  30706  numclwlk2lem2f1o  30708  nmorepnf  31098  nmoprepnf  32197  nmfnrepnf  32210  fdifsupp  33008  ressupprn  33013  disjdsct  33026  suppgsumssiun  33370  rmfsupp2  33535  domnprodn0  33576  isufd  33808  ufdprmidl  33809  1arithufdlem4  33815  dfufd2lem  33817  fedgmullem2  33998  constrconj  34113  constrelextdg2  34115  constrllcllem  34120  constrcbvlem  34123  locfinreflem  34208  sibfof  34708  signswch  34926  signstfvneq0  34937  vonf1wev  35570  vonf1owevOLD  35572  derangenlem  35641  subfacp1lem3  35652  subfacp1lem5  35654  subfacp1lem6  35655  subfacp1  35656  iscvm  35729  cvmcov  35733  cvmcov2  35745  eldm3  36231  elima4  36246  neibastop1  36848  neibastop2lem  36849  neibastop2  36850  neibastop3  36851  neifg  36860  dfttc4lem1  37017  dfttc4lem2  37018  poimirlem17  38266  poimirlem18  38267  poimirlem20  38269  poimirlem21  38270  poimirlem22  38271  poimirlem23  38272  poimirlem27  38276  poimirlem28  38277  poimirlem30  38279  poimirlem31  38280  poimirlem32  38281  mblfinlem3  38288  itg2addnclem3  38302  sstotbnd2  38403  cntotbnd  38425  heibor1lem  38438  dmecd  38937  disjecxrn  39039  br1cosscnvxrn  39191  disjimeceqim  39431  eldisjim3  39442  2llnm3N  40321  dalem4  40417  cdlemk28-3  41660  mapdh9a  42541  idomnnzpownz  42877  idomnnzgmulnz  42878  sticksstones1  42891  aks6d1c6lem1  42915  unitscyglem2  42941  unitscyglem3  42942  unitscyglem4  42943  readvcot  43103  domnexpgn0cl  43271  fsuppind  43302  dffltz  43346  pellexlem3  43538  mncn0  43846  aaitgo  43869  gneispace0nelrn2  44847  cvgdvgrat  45003  binomcxplemnotnn0  45046  disjf1  45881  disjrnmpt2  45886  disjinfi  45890  fsumiunss  46271  islptre  46315  islpcn  46333  lptre2pt  46334  0ellimcdiv  46343  liminflelimsup  46470  stoweidlem28  46722  stoweidlem43  46737  dirkercncflem2  46798  fourierdlem46  46846  fourierdlem79  46879  elaa2lem  46927  elaa2  46928  sge0fodjrnlem  47110  sge0iunmpt  47112  nnfoctbdjlem  47149  meadjiunlem  47159  meadjiun  47160  gpg5nbgrvtx13starlem1  48813  gpg5nbgrvtx13starlem3  48815  ovn0ssdmfun  48901  rmsupp0  49125  scmsuppss  49128  suppmptcfin  49133  linc1  49182  el0ldep  49223  ldepspr  49230  islindeps2  49240  zlmodzxzldeplem4  49260  zlmodzxzldep  49261  ldepsnlinclem1  49262  ldepsnlinclem2  49263  ldepsnlinc  49265  fvconstr  49617  fvconstrn0  49618  fvconstr2  49619  catprslem  49765  catprsc  49768  catprsc2  49769  oppccic  49799  relcic  49800  cicpropdlem  49804  secval  50502  cscval  50503  cotval  50504