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

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

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 2733

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

This theorem is used by:  neeq1  3018  eqnetrd  3023  iftrueb  4495  inisegn0  6092  f1ounsn  7272  f12dfv  7273  f13dfv  7274  ovn0ssdmfun  7581  resf1extb  7935  suppval1  8167  elsuppfng  8170  elsuppfn  8171  suppsnop  8179  ressuppss  8184  ressuppssdif  8186  tz7.49  8439  ereldm  8755  pw2f1olem  9084  marypha1lem  9409  wdomtr  9553  inf3lem2  9614  cantnflem1  9674  cantnf  9678  cplem2  9933  cplem2OLD  9934  dfac9  10196  kmlem12  10221  infpssrlem4  10365  fin23lem14  10392  axcc2lem  10495  axcc3  10497  domtriomlem  10501  axdc2lem  10507  ac6c4  10540  zorn2lem6  10560  rpnnen1lem4  13089  rpnnen1lem5  13090  mptnn0fsuppr  14122  hashprg  14519  hashtpg  14610  prodfn0  16043  prodfrec  16044  prodfdiv  16045  ntrivcvgtail  16049  fproddiv  16108  fprodn0  16126  fproddivf  16134  dvdsle  16460  algcvg  16731  algcvga  16734  eucalgcvga  16741  rpdvds  16815  phibndlem  16927  dfphi2  16931  pcaddlem  17046  vdwmc  17136  iscatd2  17835  brcic  17953  cicer  17961  cat1lem  18251  cat1  18252  sgrp2nmndlem5  19108  symgextf1lem  19614  pmtrmvd  19650  frgpup3lem  19971  isirred  20629  rrgsupp  20933  isdrngrd  21003  isdrngrdOLD  21005  nzerooringczr  21766  dsmmelbas  22025  dsmmacl  22027  frlmssuvc2  22081  mhpsclcl  22448  mhpmulcl  22450  elcls  23371  clsndisj  23373  elcls3  23381  neindisj2  23421  clslp  23446  cmpfi  23706  cmpfii  23707  dfconn2  23717  connsuba  23718  nconnsubb  23721  1stcelcls  23760  finlocfin  23819  locfincmp  23825  dissnlocfin  23828  locfindis  23829  ptclsg  23914  dfac14lem  23916  isfbas  24128  trfbas2  24142  isfil  24146  filss  24152  fbunfip  24168  fgval  24169  elfg  24170  isufil2  24207  ufileu  24218  filufint  24219  fmfnfm  24257  flimclslem  24283  fclsopni  24314  fclsnei  24318  fclsbas  24320  fclsrest  24323  fclscmp  24329  ufilcmp  24331  isfcf  24333  fcfnei  24334  fcfneii  24336  ptcmplem2  24352  cnextcn  24366  cnextfres1  24367  tsmsfbas  24427  iscusp  24597  cuspcvg  24599  lpbl  24802  prdsxmslem2  24828  restmetu  24869  qdensere  25068  lebnumlem3  25264  isphtpc  25295  iscmet  25585  cmetcvg  25586  equivcmet  25618  cmetcusp1  25654  cmetcusp  25655  rrxmvallem  25705  ovolicc2lem2  25819  ovolicc2lem5  25822  i1fres  26006  lhop1lem  26313  deg1ldg  26390  plyco0  26490  plyeq0lem  26509  coeeq2  26541  coe1termlem  26557  rnplynfin  26612  plyconz  26613  taylfval  26668  cxpeq0  26988  ftalem4  27385  ftalem5  27386  ftalem6  27387  isppw  27423  isnsqf  27444  sqff1o  27491  musum  27500  dchrelbas3  27547  dchrelbasd  27548  dchrelbas4  27552  dchrmulcl  27558  dchrn0  27559  dchrfi  27564  dchrptlem2  27574  dchrpt  27576  lgsne0  27644  lgsdchr  27664  2sqlem11  27738  flt4ALT  27974  fltoprm  27977  nosupbnd2lem1  28054  expsne0  28804  ishlg2  29047  ishlg  29050  elcgrabasi  29357  angmgmaddov1  29370  angmgmaddcpbl  29372  angmgmaddcl  29373  angmgmval  29376  uvtx01vtx  29960  pthdlem2lem  30335  2pthdlem1  30501  clwwlknclwwlkdif  30552  umgr2cwwkdifex  30638  3pthdlem1  30747  frgrregorufr  30908  numclwwlk2lem1lem  30925  numclwwlk2lem1  30959  numclwlk2lem2f  30960  numclwlk2lem2f1o  30962  nmorepnf  31352  nmoprepnf  32451  nmfnrepnf  32464  fdifsupp  33260  ressupprn  33265  disjdsct  33278  suppgsumssiun  33615  rmfsupp2  33780  domnprodn0  33821  isufd  34054  ufdprmidl  34055  1arithufdlem4  34061  dfufd2lem  34063  fedgmullem2  34244  constrconj  34359  constrelextdg2  34361  constrllcllem  34366  constrcbvlem  34369  locfinreflem  34454  sibfof  34955  signswch  35173  signstfvneq0  35184  vonf1wev  35860  vonf1owevOLD  35862  derangenlem  35905  subfacp1lem3  35916  subfacp1lem5  35918  subfacp1lem6  35919  subfacp1  35920  iscvm  35993  cvmcov  35997  cvmcov2  36009  eldm3  36495  elima4  36510  neibastop1  37117  neibastop2lem  37118  neibastop2  37119  neibastop3  37120  neifg  37129  dfttc4lem1  37286  dfttc4lem2  37287  mh-inf3f1  37299  poimirlem17  38523  poimirlem18  38524  poimirlem20  38526  poimirlem21  38527  poimirlem22  38528  poimirlem23  38529  poimirlem27  38533  poimirlem28  38534  poimirlem30  38536  poimirlem31  38537  poimirlem32  38538  mblfinlem3  38545  itg2addnclem3  38559  sstotbnd2  38676  cntotbnd  38698  heibor1lem  38711  dmecd  39210  disjecxrn  39312  br1cosscnvxrn  39464  disjimeceqim  39704  eldisjim3  39715  2llnm3N  40594  dalem4  40690  cdlemk28-3  41933  mapdh9a  42814  idomnnzpownz  43150  idomnnzgmulnz  43151  sticksstones1  43164  aks6d1c6lem1  43188  unitscyglem2  43214  unitscyglem3  43215  unitscyglem4  43216  readvcot  43383  domnexpgn0cl  43549  fsuppind  43580  dffltz  43624  pellexlem3  43791  mncn0  44099  aaitgo  44122  gneispace0nelrn2  45100  cvgdvgrat  45256  binomcxplemnotnn0  45299  disjf1  46141  disjrnmpt2  46146  disjinfi  46150  fsumiunss  46531  islptre  46575  islpcn  46593  lptre2pt  46594  0ellimcdiv  46603  liminflelimsup  46730  stoweidlem28  46982  stoweidlem43  46997  dirkercncflem2  47058  fourierdlem46  47106  fourierdlem79  47139  elaa2lem  47187  elaa2  47188  sge0fodjrnlem  47370  sge0iunmpt  47372  nnfoctbdjlem  47409  meadjiunlem  47419  meadjiun  47420  gpg5nbgrvtx13starlem1  49113  gpg5nbgrvtx13starlem3  49115  rmsupp0  49424  scmsuppss  49427  suppmptcfin  49432  linc1  49481  el0ldep  49522  ldepspr  49529  islindeps2  49539  zlmodzxzldeplem4  49559  zlmodzxzldep  49560  ldepsnlinclem1  49561  ldepsnlinclem2  49562  ldepsnlinc  49564  ovconstbrd  49916  ovconstbrn0d  49917  elovconstbrd  49918  catprslem  50062  catprsc  50065  catprsc2  50066  oppccic  50096  relcic  50097  cicpropdlem  50101  secval  50784  cscval  50785  cotval  50786  dvsec  50800  dvcsc  50801  dvcot  50802