Theorem neeq1d 2995

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548   ≠ wne 2936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-ne 2937

This theorem is referenced by:  neeq1  2998  eqnetrd  3003  iftrueb  4469  inisegn0  6056  f1ounsn  7219  f12dfv  7220  f13dfv  7221  resf1extb  7878  suppval1  8108  elsuppfng  8111  elsuppfn  8112  suppsnop  8120  ressuppss  8125  ressuppssdif  8127  tz7.49  8378  ereldm  8691  pw2f1olem  9013  marypha1lem  9340  wdomtr  9484  inf3lem2  9545  cantnflem1  9605  cantnf  9609  cplem2  9809  dfac9  10054  kmlem12  10079  infpssrlem4  10224  fin23lem14  10251  axcc2lem  10354  axcc3  10356  domtriomlem  10360  axdc2lem  10366  ac6c4  10399  zorn2lem6  10419  rpnnen1lem4  12925  rpnnen1lem5  12926  mptnn0fsuppr  13956  hashprg  14352  hashtpg  14442  prodfn0  15854  prodfrec  15855  prodfdiv  15856  ntrivcvgtail  15860  fproddiv  15921  fprodn0  15939  fproddivf  15947  dvdsle  16274  algcvg  16540  algcvga  16543  eucalgcvga  16550  rpdvds  16624  phibndlem  16735  dfphi2  16739  pcaddlem  16854  vdwmc  16944  iscatd2  17642  brcic  17760  cicer  17768  cat1lem  18058  cat1  18059  sgrp2nmndlem5  18895  symgextf1lem  19389  pmtrmvd  19425  frgpup3lem  19746  isirred  20393  rrgsupp  20676  isdrngrd  20741  isdrngrdOLD  20743  nzerooringczr  21458  dsmmelbas  21717  dsmmacl  21719  frlmssuvc2  21773  mhpsclcl  22138  mhpmulcl  22140  elcls  23059  clsndisj  23061  elcls3  23069  neindisj2  23109  clslp  23134  cmpfi  23394  cmpfii  23395  dfconn2  23405  connsuba  23406  nconnsubb  23409  1stcelcls  23447  finlocfin  23506  locfincmp  23512  dissnlocfin  23515  locfindis  23516  ptclsg  23601  dfac14lem  23603  isfbas  23815  trfbas2  23829  isfil  23833  filss  23839  fbunfip  23855  fgval  23856  elfg  23857  isufil2  23894  ufileu  23905  filufint  23906  fmfnfm  23944  flimclslem  23970  fclsopni  24001  fclsnei  24005  fclsbas  24007  fclsrest  24010  fclscmp  24016  ufilcmp  24018  isfcf  24020  fcfnei  24021  fcfneii  24023  ptcmplem2  24039  cnextcn  24053  cnextfres1  24054  tsmsfbas  24114  iscusp  24284  cuspcvg  24286  lpbl  24489  prdsxmslem2  24515  restmetu  24556  qdensere  24755  lebnumlem3  24951  isphtpc  24982  iscmet  25272  cmetcvg  25273  equivcmet  25305  cmetcusp1  25341  cmetcusp  25342  rrxmvallem  25392  ovolicc2lem2  25506  ovolicc2lem5  25509  i1fres  25693  lhop1lem  26001  deg1ldg  26078  plyco0  26178  plyeq0lem  26196  coeeq2  26228  coe1termlem  26244  taylfval  26345  cxpeq0  26663  ftalem4  27060  ftalem5  27061  ftalem6  27062  isppw  27098  isnsqf  27119  sqff1o  27166  musum  27175  dchrelbas3  27222  dchrelbasd  27223  dchrelbas4  27227  dchrmulcl  27233  dchrn0  27234  dchrfi  27239  dchrptlem2  27249  dchrpt  27251  lgsne0  27319  lgsdchr  27339  2sqlem11  27413  nosupbnd2lem1  27699  expsne0  28448  ishlg  28690  uvtx01vtx  29486  pthdlem2lem  29855  2pthdlem1  30018  clwwlknclwwlkdif  30069  umgr2cwwkdifex  30155  3pthdlem1  30254  frgrregorufr  30415  numclwwlk2lem1lem  30432  numclwwlk2lem1  30466  numclwlk2lem2f  30467  numclwlk2lem2f1o  30469  nmorepnf  30859  nmoprepnf  31958  nmfnrepnf  31971  fdifsupp  32779  ressupprn  32784  disjdsct  32797  suppgsumssiun  33155  rmfsupp2  33321  domnprodn0  33358  isufd  33633  ufdprmidl  33634  1arithufdlem4  33640  dfufd2lem  33642  fedgmullem2  33824  constrconj  33939  constrelextdg2  33941  constrllcllem  33946  constrcbvlem  33949  locfinreflem  34034  sibfof  34534  signswch  34755  signstfvneq0  34766  vonf1owev  35349  derangenlem  35412  subfacp1lem3  35423  subfacp1lem5  35425  subfacp1lem6  35426  subfacp1  35427  iscvm  35500  cvmcov  35504  cvmcov2  35516  eldm3  36002  elima4  36017  neibastop1  36600  neibastop2lem  36601  neibastop2  36602  neibastop3  36603  neifg  36612  dfttc4lem1  36769  dfttc4lem2  36770  poimirlem17  38017  poimirlem18  38018  poimirlem20  38020  poimirlem21  38021  poimirlem22  38022  poimirlem23  38023  poimirlem27  38027  poimirlem28  38028  poimirlem30  38030  poimirlem31  38031  poimirlem32  38032  mblfinlem3  38039  itg2addnclem3  38053  sstotbnd2  38154  cntotbnd  38176  heibor1lem  38189  dmecd  38690  disjecxrn  38792  br1cosscnvxrn  38944  disjimeceqim  39184  eldisjim3  39195  2llnm3N  40074  dalem4  40170  cdlemk28-3  41413  mapdh9a  42294  idomnnzpownz  42630  idomnnzgmulnz  42631  sticksstones1  42644  aks6d1c6lem1  42668  unitscyglem2  42694  unitscyglem3  42695  unitscyglem4  42696  readvcot  42854  domnexpgn0cl  43022  fsuppind  43053  dffltz  43097  pellexlem3  43289  mncn0  43597  aaitgo  43620  gneispace0nelrn2  44598  cvgdvgrat  44770  binomcxplemnotnn0  44813  disjf1  45642  disjrnmpt2  45647  disjinfi  45651  fsumiunss  46032  islptre  46076  islpcn  46094  lptre2pt  46095  0ellimcdiv  46104  liminflelimsup  46231  stoweidlem28  46483  stoweidlem43  46498  dirkercncflem2  46559  fourierdlem46  46607  fourierdlem79  46640  elaa2lem  46688  elaa2  46689  sge0fodjrnlem  46871  sge0iunmpt  46873  nnfoctbdjlem  46910  meadjiunlem  46920  meadjiun  46921  gpg5nbgrvtx13starlem1  48574  gpg5nbgrvtx13starlem3  48576  ovn0ssdmfun  48662  rmsupp0  48871  scmsuppss  48874  suppmptcfin  48879  linc1  48928  el0ldep  48969  ldepspr  48976  islindeps2  48986  zlmodzxzldeplem4  49006  zlmodzxzldep  49007  ldepsnlinclem1  49008  ldepsnlinclem2  49009  ldepsnlinc  49011  fvconstr  49364  fvconstrn0  49365  fvconstr2  49366  catprslem  49512  catprsc  49515  catprsc2  49516  oppccic  49546  relcic  49547  cicpropdlem  49551  secval  50249  cscval  50250  cotval  50251