Theorem neeq1d 2985

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

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

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 2702

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

This theorem is referenced by:  neeq1  2988  eqnetrd  2993  iftrueb  4504  inisegn0  6072  f1ounsn  7250  f12dfv  7251  f13dfv  7252  resf1extb  7913  suppval1  8148  elsuppfng  8151  elsuppfn  8152  suppsnop  8160  ressuppss  8165  ressuppssdif  8167  tz7.49  8416  ereldm  8727  pw2f1olem  9050  marypha1lem  9391  wdomtr  9535  inf3lem2  9589  cantnflem1  9649  cantnf  9653  cplem2  9850  dfac9  10097  kmlem12  10122  infpssrlem4  10266  fin23lem14  10293  axcc2lem  10396  axcc3  10398  domtriomlem  10402  axdc2lem  10408  ac6c4  10441  zorn2lem6  10461  rpnnen1lem4  12946  rpnnen1lem5  12947  mptnn0fsuppr  13971  hashprg  14367  hashtpg  14457  prodfn0  15867  prodfrec  15868  prodfdiv  15869  ntrivcvgtail  15873  fproddiv  15934  fprodn0  15952  fproddivf  15960  dvdsle  16287  algcvg  16553  algcvga  16556  eucalgcvga  16563  rpdvds  16637  phibndlem  16747  dfphi2  16751  pcaddlem  16866  vdwmc  16956  iscatd2  17649  brcic  17767  cicer  17775  cat1lem  18065  cat1  18066  sgrp2nmndlem5  18863  symgextf1lem  19357  pmtrmvd  19393  frgpup3lem  19714  isirred  20335  rrgsupp  20617  isdrngrd  20682  isdrngrdOLD  20684  nzerooringczr  21397  dsmmelbas  21655  dsmmacl  21657  frlmssuvc2  21711  mhpsclcl  22041  mhpmulcl  22043  elcls  22967  clsndisj  22969  elcls3  22977  neindisj2  23017  clslp  23042  cmpfi  23302  cmpfii  23303  dfconn2  23313  connsuba  23314  nconnsubb  23317  1stcelcls  23355  finlocfin  23414  locfincmp  23420  dissnlocfin  23423  locfindis  23424  ptclsg  23509  dfac14lem  23511  isfbas  23723  trfbas2  23737  isfil  23741  filss  23747  fbunfip  23763  fgval  23764  elfg  23765  isufil2  23802  ufileu  23813  filufint  23814  fmfnfm  23852  flimclslem  23878  fclsopni  23909  fclsnei  23913  fclsbas  23915  fclsrest  23918  fclscmp  23924  ufilcmp  23926  isfcf  23928  fcfnei  23929  fcfneii  23931  ptcmplem2  23947  cnextcn  23961  cnextfres1  23962  tsmsfbas  24022  iscusp  24193  cuspcvg  24195  lpbl  24398  prdsxmslem2  24424  restmetu  24465  qdensere  24664  lebnumlem3  24869  isphtpc  24900  iscmet  25191  cmetcvg  25192  equivcmet  25224  cmetcusp1  25260  cmetcusp  25261  rrxmvallem  25311  ovolicc2lem2  25426  ovolicc2lem5  25429  i1fres  25613  lhop1lem  25925  deg1ldg  26004  plyco0  26104  plyeq0lem  26122  coeeq2  26154  coe1termlem  26170  taylfval  26273  cxpeq0  26594  ftalem4  26993  ftalem5  26994  ftalem6  26995  isppw  27031  isnsqf  27052  sqff1o  27099  musum  27108  dchrelbas3  27156  dchrelbasd  27157  dchrelbas4  27161  dchrmulcl  27167  dchrn0  27168  dchrfi  27173  dchrptlem2  27183  dchrpt  27185  lgsne0  27253  lgsdchr  27273  2sqlem11  27347  nosupbnd2lem1  27634  expsne0  28328  ishlg  28536  uvtx01vtx  29331  pthdlem2lem  29704  2pthdlem1  29867  clwwlknclwwlkdif  29915  umgr2cwwkdifex  30001  3pthdlem1  30100  frgrregorufr  30261  numclwwlk2lem1lem  30278  numclwwlk2lem1  30312  numclwlk2lem2f  30313  numclwlk2lem2f1o  30315  nmorepnf  30704  nmoprepnf  31803  nmfnrepnf  31816  fdifsupp  32615  ressupprn  32620  disjdsct  32633  rmfsupp2  33196  domnprodn0  33233  isufd  33518  ufdprmidl  33519  1arithufdlem4  33525  dfufd2lem  33527  fedgmullem2  33633  constrconj  33742  constrelextdg2  33744  constrllcllem  33749  constrcbvlem  33752  locfinreflem  33837  sibfof  34338  signswch  34559  signstfvneq0  34570  vonf1owev  35102  derangenlem  35165  subfacp1lem3  35176  subfacp1lem5  35178  subfacp1lem6  35179  subfacp1  35180  iscvm  35253  cvmcov  35257  cvmcov2  35269  eldm3  35755  elima4  35770  neibastop1  36354  neibastop2lem  36355  neibastop2  36356  neibastop3  36357  neifg  36366  poimirlem17  37638  poimirlem18  37639  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem23  37644  poimirlem27  37648  poimirlem28  37649  poimirlem30  37651  poimirlem31  37652  poimirlem32  37653  mblfinlem3  37660  itg2addnclem3  37674  sstotbnd2  37775  cntotbnd  37797  heibor1lem  37810  dmecd  38299  disjecxrn  38382  br1cosscnvxrn  38472  2llnm3N  39570  dalem4  39666  cdlemk28-3  40909  mapdh9a  41790  idomnnzpownz  42127  idomnnzgmulnz  42128  sticksstones1  42141  aks6d1c6lem1  42165  unitscyglem2  42191  unitscyglem3  42192  unitscyglem4  42193  readvcot  42359  domnexpgn0cl  42518  fsuppind  42585  dffltz  42629  pellexlem3  42826  mncn0  43135  aaitgo  43158  gneispace0nelrn2  44137  cvgdvgrat  44309  binomcxplemnotnn0  44352  disjf1  45184  disjrnmpt2  45189  disjinfi  45193  fsumiunss  45580  islptre  45624  islpcn  45644  lptre2pt  45645  0ellimcdiv  45654  liminflelimsup  45781  stoweidlem28  46033  stoweidlem43  46048  dirkercncflem2  46109  fourierdlem46  46157  fourierdlem79  46190  elaa2lem  46238  elaa2  46239  sge0fodjrnlem  46421  sge0iunmpt  46423  nnfoctbdjlem  46460  meadjiunlem  46470  meadjiun  46471  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem3  48068  ovn0ssdmfun  48151  rmsupp0  48360  scmsuppss  48363  suppmptcfin  48368  linc1  48418  el0ldep  48459  ldepspr  48466  islindeps2  48476  zlmodzxzldeplem4  48496  zlmodzxzldep  48497  ldepsnlinclem1  48498  ldepsnlinclem2  48499  ldepsnlinc  48501  fvconstr  48854  fvconstrn0  48855  fvconstr2  48856  catprslem  49003  catprsc  49006  catprsc2  49007  oppccic  49037  relcic  49038  cicpropdlem  49042  secval  49740  cscval  49741  cotval  49742