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

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

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  neeq1  2994  eqnetrd  2999  iftrueb  4513  inisegn0  6085  f1ounsn  7265  f12dfv  7266  f13dfv  7267  resf1extb  7930  suppval1  8165  elsuppfng  8168  elsuppfn  8169  suppsnop  8177  ressuppss  8182  ressuppssdif  8184  tz7.49  8459  ereldm  8769  pw2f1olem  9090  marypha1lem  9445  wdomtr  9589  inf3lem2  9643  cantnflem1  9703  cantnf  9707  cplem2  9904  dfac9  10151  kmlem12  10176  infpssrlem4  10320  fin23lem14  10347  axcc2lem  10450  axcc3  10452  domtriomlem  10456  axdc2lem  10462  ac6c4  10495  zorn2lem6  10515  rpnnen1lem4  12996  rpnnen1lem5  12997  mptnn0fsuppr  14017  hashprg  14413  hashtpg  14503  prodfn0  15910  prodfrec  15911  prodfdiv  15912  ntrivcvgtail  15916  fproddiv  15977  fprodn0  15995  fproddivf  16003  dvdsle  16329  algcvg  16595  algcvga  16598  eucalgcvga  16605  rpdvds  16679  phibndlem  16789  dfphi2  16793  pcaddlem  16908  vdwmc  16998  iscatd2  17693  brcic  17811  cicer  17819  cat1lem  18109  cat1  18110  sgrp2nmndlem5  18907  symgextf1lem  19401  pmtrmvd  19437  frgpup3lem  19758  isirred  20379  rrgsupp  20661  isdrngrd  20726  isdrngrdOLD  20728  nzerooringczr  21441  dsmmelbas  21699  dsmmacl  21701  frlmssuvc2  21755  mhpsclcl  22085  mhpmulcl  22087  elcls  23011  clsndisj  23013  elcls3  23021  neindisj2  23061  clslp  23086  cmpfi  23346  cmpfii  23347  dfconn2  23357  connsuba  23358  nconnsubb  23361  1stcelcls  23399  finlocfin  23458  locfincmp  23464  dissnlocfin  23467  locfindis  23468  ptclsg  23553  dfac14lem  23555  isfbas  23767  trfbas2  23781  isfil  23785  filss  23791  fbunfip  23807  fgval  23808  elfg  23809  isufil2  23846  ufileu  23857  filufint  23858  fmfnfm  23896  flimclslem  23922  fclsopni  23953  fclsnei  23957  fclsbas  23959  fclsrest  23962  fclscmp  23968  ufilcmp  23970  isfcf  23972  fcfnei  23973  fcfneii  23975  ptcmplem2  23991  cnextcn  24005  cnextfres1  24006  tsmsfbas  24066  iscusp  24237  cuspcvg  24239  lpbl  24442  prdsxmslem2  24468  restmetu  24509  qdensere  24708  lebnumlem3  24913  isphtpc  24944  iscmet  25236  cmetcvg  25237  equivcmet  25269  cmetcusp1  25305  cmetcusp  25306  rrxmvallem  25356  ovolicc2lem2  25471  ovolicc2lem5  25474  i1fres  25658  lhop1lem  25970  deg1ldg  26049  plyco0  26149  plyeq0lem  26167  coeeq2  26199  coe1termlem  26215  taylfval  26318  cxpeq0  26639  ftalem4  27038  ftalem5  27039  ftalem6  27040  isppw  27076  isnsqf  27097  sqff1o  27144  musum  27153  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  28373  ishlg  28581  uvtx01vtx  29376  pthdlem2lem  29749  2pthdlem1  29912  clwwlknclwwlkdif  29960  umgr2cwwkdifex  30046  3pthdlem1  30145  frgrregorufr  30306  numclwwlk2lem1lem  30323  numclwwlk2lem1  30357  numclwlk2lem2f  30358  numclwlk2lem2f1o  30360  nmorepnf  30749  nmoprepnf  31848  nmfnrepnf  31861  fdifsupp  32662  ressupprn  32667  disjdsct  32680  rmfsupp2  33233  domnprodn0  33270  isufd  33555  ufdprmidl  33556  1arithufdlem4  33562  dfufd2lem  33564  fedgmullem2  33670  constrconj  33779  constrelextdg2  33781  constrllcllem  33786  constrcbvlem  33789  locfinreflem  33871  sibfof  34372  signswch  34593  signstfvneq0  34604  derangenlem  35193  subfacp1lem3  35204  subfacp1lem5  35206  subfacp1lem6  35207  subfacp1  35208  iscvm  35281  cvmcov  35285  cvmcov2  35297  eldm3  35778  elima4  35793  neibastop1  36377  neibastop2lem  36378  neibastop2  36379  neibastop3  36380  neifg  36389  poimirlem17  37661  poimirlem18  37662  poimirlem20  37664  poimirlem21  37665  poimirlem22  37666  poimirlem23  37667  poimirlem27  37671  poimirlem28  37672  poimirlem30  37674  poimirlem31  37675  poimirlem32  37676  mblfinlem3  37683  itg2addnclem3  37697  sstotbnd2  37798  cntotbnd  37820  heibor1lem  37833  dmecd  38322  disjecxrn  38407  br1cosscnvxrn  38492  2llnm3N  39588  dalem4  39684  cdlemk28-3  40927  mapdh9a  41808  idomnnzpownz  42145  idomnnzgmulnz  42146  sticksstones1  42159  aks6d1c6lem1  42183  unitscyglem2  42209  unitscyglem3  42210  unitscyglem4  42211  metakunt29  42246  readvcot  42407  domnexpgn0cl  42546  fsuppind  42613  dffltz  42657  pellexlem3  42854  mncn0  43163  aaitgo  43186  gneispace0nelrn2  44165  cvgdvgrat  44337  binomcxplemnotnn0  44380  disjf1  45207  disjrnmpt2  45212  disjinfi  45216  fsumiunss  45604  islptre  45648  islpcn  45668  lptre2pt  45669  0ellimcdiv  45678  liminflelimsup  45805  stoweidlem28  46057  stoweidlem43  46072  dirkercncflem2  46133  fourierdlem46  46181  fourierdlem79  46214  elaa2lem  46262  elaa2  46263  sge0fodjrnlem  46445  sge0iunmpt  46447  nnfoctbdjlem  46484  meadjiunlem  46494  meadjiun  46495  gpg5nbgrvtx13starlem1  48073  gpg5nbgrvtx13starlem3  48075  ovn0ssdmfun  48134  rmsupp0  48343  scmsuppss  48346  suppmptcfin  48351  linc1  48401  el0ldep  48442  ldepspr  48449  islindeps2  48459  zlmodzxzldeplem4  48479  zlmodzxzldep  48480  ldepsnlinclem1  48481  ldepsnlinclem2  48482  ldepsnlinc  48484  fvconstr  48838  fvconstrn0  48839  fvconstr2  48840  catprslem  48985  catprsc  48988  catprsc2  48989  oppccic  49011  relcic  49012  cicpropdlem  49016  secval  49611  cscval  49612  cotval  49613