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 206   = wceq 1542   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ne 2933

This theorem is referenced by:  neeq1  2994  eqnetrd  2999  iftrueb  4479  inisegn0  6063  f1ounsn  7227  f12dfv  7228  f13dfv  7229  resf1extb  7885  suppval1  8116  elsuppfng  8119  elsuppfn  8120  suppsnop  8128  ressuppss  8133  ressuppssdif  8135  tz7.49  8384  ereldm  8697  pw2f1olem  9019  marypha1lem  9346  wdomtr  9490  inf3lem2  9550  cantnflem1  9610  cantnf  9614  cplem2  9814  dfac9  10059  kmlem12  10084  infpssrlem4  10228  fin23lem14  10255  axcc2lem  10358  axcc3  10360  domtriomlem  10364  axdc2lem  10370  ac6c4  10403  zorn2lem6  10423  rpnnen1lem4  12930  rpnnen1lem5  12931  mptnn0fsuppr  13961  hashprg  14357  hashtpg  14447  prodfn0  15859  prodfrec  15860  prodfdiv  15861  ntrivcvgtail  15865  fproddiv  15926  fprodn0  15944  fproddivf  15952  dvdsle  16279  algcvg  16545  algcvga  16548  eucalgcvga  16555  rpdvds  16629  phibndlem  16740  dfphi2  16744  pcaddlem  16859  vdwmc  16949  iscatd2  17647  brcic  17765  cicer  17773  cat1lem  18063  cat1  18064  sgrp2nmndlem5  18900  symgextf1lem  19395  pmtrmvd  19431  frgpup3lem  19752  isirred  20399  rrgsupp  20678  isdrngrd  20743  isdrngrdOLD  20745  nzerooringczr  21460  dsmmelbas  21719  dsmmacl  21721  frlmssuvc2  21775  mhpsclcl  22113  mhpmulcl  22115  elcls  23038  clsndisj  23040  elcls3  23048  neindisj2  23088  clslp  23113  cmpfi  23373  cmpfii  23374  dfconn2  23384  connsuba  23385  nconnsubb  23388  1stcelcls  23426  finlocfin  23485  locfincmp  23491  dissnlocfin  23494  locfindis  23495  ptclsg  23580  dfac14lem  23582  isfbas  23794  trfbas2  23808  isfil  23812  filss  23818  fbunfip  23834  fgval  23835  elfg  23836  isufil2  23873  ufileu  23884  filufint  23885  fmfnfm  23923  flimclslem  23949  fclsopni  23980  fclsnei  23984  fclsbas  23986  fclsrest  23989  fclscmp  23995  ufilcmp  23997  isfcf  23999  fcfnei  24000  fcfneii  24002  ptcmplem2  24018  cnextcn  24032  cnextfres1  24033  tsmsfbas  24093  iscusp  24263  cuspcvg  24265  lpbl  24468  prdsxmslem2  24494  restmetu  24535  qdensere  24734  lebnumlem3  24930  isphtpc  24961  iscmet  25251  cmetcvg  25252  equivcmet  25284  cmetcusp1  25320  cmetcusp  25321  rrxmvallem  25371  ovolicc2lem2  25485  ovolicc2lem5  25488  i1fres  25672  lhop1lem  25980  deg1ldg  26057  plyco0  26157  plyeq0lem  26175  coeeq2  26207  coe1termlem  26223  taylfval  26324  cxpeq0  26642  ftalem4  27039  ftalem5  27040  ftalem6  27041  isppw  27077  isnsqf  27098  sqff1o  27145  musum  27154  dchrelbas3  27201  dchrelbasd  27202  dchrelbas4  27206  dchrmulcl  27212  dchrn0  27213  dchrfi  27218  dchrptlem2  27228  dchrpt  27230  lgsne0  27298  lgsdchr  27318  2sqlem11  27392  nosupbnd2lem1  27679  expsne0  28428  ishlg  28670  uvtx01vtx  29466  pthdlem2lem  29835  2pthdlem1  29998  clwwlknclwwlkdif  30049  umgr2cwwkdifex  30135  3pthdlem1  30234  frgrregorufr  30395  numclwwlk2lem1lem  30412  numclwwlk2lem1  30446  numclwlk2lem2f  30447  numclwlk2lem2f1o  30449  nmorepnf  30839  nmoprepnf  31938  nmfnrepnf  31951  fdifsupp  32758  ressupprn  32763  disjdsct  32776  suppgsumssiun  33133  rmfsupp2  33299  domnprodn0  33336  isufd  33600  ufdprmidl  33601  1arithufdlem4  33607  dfufd2lem  33609  fedgmullem2  33774  constrconj  33889  constrelextdg2  33891  constrllcllem  33896  constrcbvlem  33899  locfinreflem  33984  sibfof  34484  signswch  34705  signstfvneq0  34716  vonf1owev  35290  derangenlem  35353  subfacp1lem3  35364  subfacp1lem5  35366  subfacp1lem6  35367  subfacp1  35368  iscvm  35441  cvmcov  35445  cvmcov2  35457  eldm3  35943  elima4  35958  neibastop1  36541  neibastop2lem  36542  neibastop2  36543  neibastop3  36544  neifg  36553  dfttc4lem1  36710  dfttc4lem2  36711  poimirlem17  37958  poimirlem18  37959  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem23  37964  poimirlem27  37968  poimirlem28  37969  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  mblfinlem3  37980  itg2addnclem3  37994  sstotbnd2  38095  cntotbnd  38117  heibor1lem  38130  dmecd  38631  disjecxrn  38733  br1cosscnvxrn  38885  disjimeceqim  39125  eldisjim3  39136  2llnm3N  40015  dalem4  40111  cdlemk28-3  41354  mapdh9a  42235  idomnnzpownz  42571  idomnnzgmulnz  42572  sticksstones1  42585  aks6d1c6lem1  42609  unitscyglem2  42635  unitscyglem3  42636  unitscyglem4  42637  readvcot  42796  domnexpgn0cl  42968  fsuppind  43023  dffltz  43067  pellexlem3  43259  mncn0  43567  aaitgo  43590  gneispace0nelrn2  44568  cvgdvgrat  44740  binomcxplemnotnn0  44783  disjf1  45613  disjrnmpt2  45618  disjinfi  45622  fsumiunss  46005  islptre  46049  islpcn  46067  lptre2pt  46068  0ellimcdiv  46077  liminflelimsup  46204  stoweidlem28  46456  stoweidlem43  46471  dirkercncflem2  46532  fourierdlem46  46580  fourierdlem79  46613  elaa2lem  46661  elaa2  46662  sge0fodjrnlem  46844  sge0iunmpt  46846  nnfoctbdjlem  46883  meadjiunlem  46893  meadjiun  46894  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem3  48549  ovn0ssdmfun  48635  rmsupp0  48844  scmsuppss  48847  suppmptcfin  48852  linc1  48901  el0ldep  48942  ldepspr  48949  islindeps2  48959  zlmodzxzldeplem4  48979  zlmodzxzldep  48980  ldepsnlinclem1  48981  ldepsnlinclem2  48982  ldepsnlinc  48984  fvconstr  49337  fvconstrn0  49338  fvconstr2  49339  catprslem  49485  catprsc  49488  catprsc2  49489  oppccic  49519  relcic  49520  cicpropdlem  49524  secval  50222  cscval  50223  cotval  50224