Theorem neeq1d 2984

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  neeq1  2987  eqnetrd  2992  iftrueb  4501  inisegn0  6069  f1ounsn  7247  f12dfv  7248  f13dfv  7249  resf1extb  7910  suppval1  8145  elsuppfng  8148  elsuppfn  8149  suppsnop  8157  ressuppss  8162  ressuppssdif  8164  tz7.49  8413  ereldm  8724  pw2f1olem  9045  marypha1lem  9384  wdomtr  9528  inf3lem2  9582  cantnflem1  9642  cantnf  9646  cplem2  9843  dfac9  10090  kmlem12  10115  infpssrlem4  10259  fin23lem14  10286  axcc2lem  10389  axcc3  10391  domtriomlem  10395  axdc2lem  10401  ac6c4  10434  zorn2lem6  10454  rpnnen1lem4  12939  rpnnen1lem5  12940  mptnn0fsuppr  13964  hashprg  14360  hashtpg  14450  prodfn0  15860  prodfrec  15861  prodfdiv  15862  ntrivcvgtail  15866  fproddiv  15927  fprodn0  15945  fproddivf  15953  dvdsle  16280  algcvg  16546  algcvga  16549  eucalgcvga  16556  rpdvds  16630  phibndlem  16740  dfphi2  16744  pcaddlem  16859  vdwmc  16949  iscatd2  17642  brcic  17760  cicer  17768  cat1lem  18058  cat1  18059  sgrp2nmndlem5  18856  symgextf1lem  19350  pmtrmvd  19386  frgpup3lem  19707  isirred  20328  rrgsupp  20610  isdrngrd  20675  isdrngrdOLD  20677  nzerooringczr  21390  dsmmelbas  21648  dsmmacl  21650  frlmssuvc2  21704  mhpsclcl  22034  mhpmulcl  22036  elcls  22960  clsndisj  22962  elcls3  22970  neindisj2  23010  clslp  23035  cmpfi  23295  cmpfii  23296  dfconn2  23306  connsuba  23307  nconnsubb  23310  1stcelcls  23348  finlocfin  23407  locfincmp  23413  dissnlocfin  23416  locfindis  23417  ptclsg  23502  dfac14lem  23504  isfbas  23716  trfbas2  23730  isfil  23734  filss  23740  fbunfip  23756  fgval  23757  elfg  23758  isufil2  23795  ufileu  23806  filufint  23807  fmfnfm  23845  flimclslem  23871  fclsopni  23902  fclsnei  23906  fclsbas  23908  fclsrest  23911  fclscmp  23917  ufilcmp  23919  isfcf  23921  fcfnei  23922  fcfneii  23924  ptcmplem2  23940  cnextcn  23954  cnextfres1  23955  tsmsfbas  24015  iscusp  24186  cuspcvg  24188  lpbl  24391  prdsxmslem2  24417  restmetu  24458  qdensere  24657  lebnumlem3  24862  isphtpc  24893  iscmet  25184  cmetcvg  25185  equivcmet  25217  cmetcusp1  25253  cmetcusp  25254  rrxmvallem  25304  ovolicc2lem2  25419  ovolicc2lem5  25422  i1fres  25606  lhop1lem  25918  deg1ldg  25997  plyco0  26097  plyeq0lem  26115  coeeq2  26147  coe1termlem  26163  taylfval  26266  cxpeq0  26587  ftalem4  26986  ftalem5  26987  ftalem6  26988  isppw  27024  isnsqf  27045  sqff1o  27092  musum  27101  dchrelbas3  27149  dchrelbasd  27150  dchrelbas4  27154  dchrmulcl  27160  dchrn0  27161  dchrfi  27166  dchrptlem2  27176  dchrpt  27178  lgsne0  27246  lgsdchr  27266  2sqlem11  27340  nosupbnd2lem1  27627  expsne0  28321  ishlg  28529  uvtx01vtx  29324  pthdlem2lem  29697  2pthdlem1  29860  clwwlknclwwlkdif  29908  umgr2cwwkdifex  29994  3pthdlem1  30093  frgrregorufr  30254  numclwwlk2lem1lem  30271  numclwwlk2lem1  30305  numclwlk2lem2f  30306  numclwlk2lem2f1o  30308  nmorepnf  30697  nmoprepnf  31796  nmfnrepnf  31809  fdifsupp  32608  ressupprn  32613  disjdsct  32626  rmfsupp2  33189  domnprodn0  33226  isufd  33511  ufdprmidl  33512  1arithufdlem4  33518  dfufd2lem  33520  fedgmullem2  33626  constrconj  33735  constrelextdg2  33737  constrllcllem  33742  constrcbvlem  33745  locfinreflem  33830  sibfof  34331  signswch  34552  signstfvneq0  34563  vonf1owev  35095  derangenlem  35158  subfacp1lem3  35169  subfacp1lem5  35171  subfacp1lem6  35172  subfacp1  35173  iscvm  35246  cvmcov  35250  cvmcov2  35262  eldm3  35748  elima4  35763  neibastop1  36347  neibastop2lem  36348  neibastop2  36349  neibastop3  36350  neifg  36359  poimirlem17  37631  poimirlem18  37632  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem23  37637  poimirlem27  37641  poimirlem28  37642  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  mblfinlem3  37653  itg2addnclem3  37667  sstotbnd2  37768  cntotbnd  37790  heibor1lem  37803  dmecd  38292  disjecxrn  38375  br1cosscnvxrn  38465  2llnm3N  39563  dalem4  39659  cdlemk28-3  40902  mapdh9a  41783  idomnnzpownz  42120  idomnnzgmulnz  42121  sticksstones1  42134  aks6d1c6lem1  42158  unitscyglem2  42184  unitscyglem3  42185  unitscyglem4  42186  readvcot  42352  domnexpgn0cl  42511  fsuppind  42578  dffltz  42622  pellexlem3  42819  mncn0  43128  aaitgo  43151  gneispace0nelrn2  44130  cvgdvgrat  44302  binomcxplemnotnn0  44345  disjf1  45177  disjrnmpt2  45182  disjinfi  45186  fsumiunss  45573  islptre  45617  islpcn  45637  lptre2pt  45638  0ellimcdiv  45647  liminflelimsup  45774  stoweidlem28  46026  stoweidlem43  46041  dirkercncflem2  46102  fourierdlem46  46150  fourierdlem79  46183  elaa2lem  46231  elaa2  46232  sge0fodjrnlem  46414  sge0iunmpt  46416  nnfoctbdjlem  46453  meadjiunlem  46463  meadjiun  46464  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem3  48064  ovn0ssdmfun  48147  rmsupp0  48356  scmsuppss  48359  suppmptcfin  48364  linc1  48414  el0ldep  48455  ldepspr  48462  islindeps2  48472  zlmodzxzldeplem4  48492  zlmodzxzldep  48493  ldepsnlinclem1  48494  ldepsnlinclem2  48495  ldepsnlinc  48497  fvconstr  48850  fvconstrn0  48851  fvconstr2  48852  catprslem  48999  catprsc  49002  catprsc2  49003  oppccic  49033  relcic  49034  cicpropdlem  49038  secval  49736  cscval  49737  cotval  49738