Theorem neeq1d 2991

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543   ≠ wne 2932

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 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728  df-ne 2933

This theorem is referenced by:  neeq1  2994  eqnetrd  2999  inisegn0  5946  f12dfv  7062  f13dfv  7063  suppval1  7887  elsuppfng  7890  elsuppfn  7891  suppsnop  7898  ressuppss  7903  ressuppssdif  7905  tz7.49  8159  ereldm  8417  pw2f1olem  8727  marypha1lem  9027  wdomtr  9169  inf3lem2  9222  cantnflem1  9282  cantnf  9286  cplem2  9471  dfac9  9715  kmlem12  9740  infpssrlem4  9885  fin23lem14  9912  axcc2lem  10015  axcc3  10017  domtriomlem  10021  axdc2lem  10027  ac6c4  10060  zorn2lem6  10080  rpnnen1lem4  12541  rpnnen1lem5  12542  mptnn0fsuppr  13537  hashprg  13927  hashtpg  14016  prodfn0  15421  prodfrec  15422  prodfdiv  15423  ntrivcvgtail  15427  fproddiv  15486  fprodn0  15504  fproddivf  15512  dvdsle  15834  algcvg  16096  algcvga  16099  eucalgcvga  16106  rpdvds  16180  phibndlem  16286  dfphi2  16290  pcaddlem  16404  vdwmc  16494  iscatd2  17138  brcic  17257  cicer  17265  cat1lem  17556  cat1  17557  sgrp2nmndlem5  18310  symgextf1lem  18766  pmtrmvd  18802  frgpup3lem  19121  isirred  19671  isdrngrd  19747  rrgsupp  20283  dsmmelbas  20655  dsmmacl  20657  frlmssuvc2  20711  mhpsclcl  21041  mhpmulcl  21043  elcls  21924  clsndisj  21926  elcls3  21934  neindisj2  21974  clslp  21999  cmpfi  22259  cmpfii  22260  dfconn2  22270  connsuba  22271  nconnsubb  22274  1stcelcls  22312  finlocfin  22371  locfincmp  22377  dissnlocfin  22380  locfindis  22381  ptclsg  22466  dfac14lem  22468  isfbas  22680  trfbas2  22694  isfil  22698  filss  22704  fbunfip  22720  fgval  22721  elfg  22722  isufil2  22759  ufileu  22770  filufint  22771  fmfnfm  22809  flimclslem  22835  fclsopni  22866  fclsnei  22870  fclsbas  22872  fclsrest  22875  fclscmp  22881  ufilcmp  22883  isfcf  22885  fcfnei  22886  fcfneii  22888  ptcmplem2  22904  cnextcn  22918  cnextfres1  22919  tsmsfbas  22979  iscusp  23150  cuspcvg  23152  lpbl  23355  prdsxmslem2  23381  restmetu  23422  qdensere  23621  lebnumlem3  23814  isphtpc  23845  iscmet  24135  cmetcvg  24136  equivcmet  24168  cmetcusp1  24204  cmetcusp  24205  rrxmvallem  24255  ovolicc2lem2  24369  ovolicc2lem5  24372  i1fres  24557  lhop1lem  24864  deg1ldg  24944  plyco0  25040  plyeq0lem  25058  coeeq2  25090  coe1termlem  25106  taylfval  25205  cxpeq0  25520  ftalem4  25912  ftalem5  25913  ftalem6  25914  isppw  25950  isnsqf  25971  sqff1o  26018  musum  26027  dchrelbas3  26073  dchrelbasd  26074  dchrelbas4  26078  dchrmulcl  26084  dchrn0  26085  dchrfi  26090  dchrptlem2  26100  dchrpt  26102  lgsne0  26170  lgsdchr  26190  2sqlem11  26264  ishlg  26647  uvtx01vtx  27439  pthdlem2lem  27808  2pthdlem1  27968  clwwlknclwwlkdif  28016  umgr2cwwkdifex  28102  3pthdlem1  28201  frgrregorufr  28362  numclwwlk2lem1lem  28379  numclwwlk2lem1  28413  numclwlk2lem2f  28414  numclwlk2lem2f1o  28416  nmorepnf  28803  nmoprepnf  29902  nmfnrepnf  29915  ressupprn  30698  disjdsct  30709  rmfsupp2  31165  isufd  31331  fedgmullem2  31379  locfinreflem  31458  sibfof  31973  signswch  32206  signstfvneq0  32217  derangenlem  32800  subfacp1lem3  32811  subfacp1lem5  32813  subfacp1lem6  32814  subfacp1  32815  iscvm  32888  cvmcov  32892  cvmcov2  32904  eldm3  33398  elima4  33420  nosupbnd2lem1  33604  neibastop1  34234  neibastop2lem  34235  neibastop2  34236  neibastop3  34237  neifg  34246  poimirlem17  35480  poimirlem18  35481  poimirlem20  35483  poimirlem21  35484  poimirlem22  35485  poimirlem23  35486  poimirlem27  35490  poimirlem28  35491  poimirlem30  35493  poimirlem31  35494  poimirlem32  35495  mblfinlem3  35502  itg2addnclem3  35516  sstotbnd2  35618  cntotbnd  35640  heibor1lem  35653  dmecd  36126  br1cosscnvxrn  36278  2llnm3N  37269  dalem4  37365  cdlemk28-3  38608  mapdh9a  39489  sticksstones1  39771  metakunt29  39816  fsuppind  39930  dffltz  40115  pellexlem3  40297  mncn0  40608  aaitgo  40631  gneispace0nelrn2  41369  cvgdvgrat  41545  binomcxplemnotnn0  41588  disjf1  42334  disjrnmpt2  42340  disjinfi  42345  fsumiunss  42734  islptre  42778  islpcn  42798  lptre2pt  42799  0ellimcdiv  42808  liminflelimsup  42935  stoweidlem28  43187  stoweidlem43  43202  dirkercncflem2  43263  fourierdlem46  43311  fourierdlem79  43344  elaa2lem  43392  elaa2  43393  sge0fodjrnlem  43572  sge0iunmpt  43574  nnfoctbdjlem  43611  meadjiunlem  43621  meadjiun  43622  ovn0ssdmfun  44937  nzerooringczr  45246  rmsupp0  45320  scmsuppss  45324  suppmptcfin  45331  linc1  45382  el0ldep  45423  ldepspr  45430  islindeps2  45440  zlmodzxzldeplem4  45460  zlmodzxzldep  45461  ldepsnlinclem1  45462  ldepsnlinclem2  45463  ldepsnlinc  45465  fvconstr  45799  fvconstrn0  45800  fvconstr2  45801  catprslem  45907  catprsc  45910  catprsc2  45911  secval  46063  cscval  46064  cotval  46065