Theorem neeq1d 2987

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ≠ wne 2928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ne 2929

This theorem is referenced by:  neeq1  2990  eqnetrd  2995  iftrueb  4488  inisegn0  6047  f1ounsn  7206  f12dfv  7207  f13dfv  7208  resf1extb  7864  suppval1  8096  elsuppfng  8099  elsuppfn  8100  suppsnop  8108  ressuppss  8113  ressuppssdif  8115  tz7.49  8364  ereldm  8675  pw2f1olem  8994  marypha1lem  9317  wdomtr  9461  inf3lem2  9519  cantnflem1  9579  cantnf  9583  cplem2  9780  dfac9  10025  kmlem12  10050  infpssrlem4  10194  fin23lem14  10221  axcc2lem  10324  axcc3  10326  domtriomlem  10330  axdc2lem  10336  ac6c4  10369  zorn2lem6  10389  rpnnen1lem4  12875  rpnnen1lem5  12876  mptnn0fsuppr  13903  hashprg  14299  hashtpg  14389  prodfn0  15798  prodfrec  15799  prodfdiv  15800  ntrivcvgtail  15804  fproddiv  15865  fprodn0  15883  fproddivf  15891  dvdsle  16218  algcvg  16484  algcvga  16487  eucalgcvga  16494  rpdvds  16568  phibndlem  16678  dfphi2  16682  pcaddlem  16797  vdwmc  16887  iscatd2  17584  brcic  17702  cicer  17710  cat1lem  18000  cat1  18001  sgrp2nmndlem5  18834  symgextf1lem  19330  pmtrmvd  19366  frgpup3lem  19687  isirred  20335  rrgsupp  20614  isdrngrd  20679  isdrngrdOLD  20681  nzerooringczr  21415  dsmmelbas  21674  dsmmacl  21676  frlmssuvc2  21730  mhpsclcl  22060  mhpmulcl  22062  elcls  22986  clsndisj  22988  elcls3  22996  neindisj2  23036  clslp  23061  cmpfi  23321  cmpfii  23322  dfconn2  23332  connsuba  23333  nconnsubb  23336  1stcelcls  23374  finlocfin  23433  locfincmp  23439  dissnlocfin  23442  locfindis  23443  ptclsg  23528  dfac14lem  23530  isfbas  23742  trfbas2  23756  isfil  23760  filss  23766  fbunfip  23782  fgval  23783  elfg  23784  isufil2  23821  ufileu  23832  filufint  23833  fmfnfm  23871  flimclslem  23897  fclsopni  23928  fclsnei  23932  fclsbas  23934  fclsrest  23937  fclscmp  23943  ufilcmp  23945  isfcf  23947  fcfnei  23948  fcfneii  23950  ptcmplem2  23966  cnextcn  23980  cnextfres1  23981  tsmsfbas  24041  iscusp  24211  cuspcvg  24213  lpbl  24416  prdsxmslem2  24442  restmetu  24483  qdensere  24682  lebnumlem3  24887  isphtpc  24918  iscmet  25209  cmetcvg  25210  equivcmet  25242  cmetcusp1  25278  cmetcusp  25279  rrxmvallem  25329  ovolicc2lem2  25444  ovolicc2lem5  25447  i1fres  25631  lhop1lem  25943  deg1ldg  26022  plyco0  26122  plyeq0lem  26140  coeeq2  26172  coe1termlem  26188  taylfval  26291  cxpeq0  26612  ftalem4  27011  ftalem5  27012  ftalem6  27013  isppw  27049  isnsqf  27070  sqff1o  27117  musum  27126  dchrelbas3  27174  dchrelbasd  27175  dchrelbas4  27179  dchrmulcl  27185  dchrn0  27186  dchrfi  27191  dchrptlem2  27201  dchrpt  27203  lgsne0  27271  lgsdchr  27291  2sqlem11  27365  nosupbnd2lem1  27652  expsne0  28357  ishlg  28578  uvtx01vtx  29373  pthdlem2lem  29743  2pthdlem1  29906  clwwlknclwwlkdif  29954  umgr2cwwkdifex  30040  3pthdlem1  30139  frgrregorufr  30300  numclwwlk2lem1lem  30317  numclwwlk2lem1  30351  numclwlk2lem2f  30352  numclwlk2lem2f1o  30354  nmorepnf  30743  nmoprepnf  31842  nmfnrepnf  31855  fdifsupp  32661  ressupprn  32666  disjdsct  32679  rmfsupp2  33200  domnprodn0  33237  isufd  33500  ufdprmidl  33501  1arithufdlem4  33507  dfufd2lem  33509  fedgmullem2  33638  constrconj  33753  constrelextdg2  33755  constrllcllem  33760  constrcbvlem  33763  locfinreflem  33848  sibfof  34348  signswch  34569  signstfvneq0  34580  vonf1owev  35140  derangenlem  35203  subfacp1lem3  35214  subfacp1lem5  35216  subfacp1lem6  35217  subfacp1  35218  iscvm  35291  cvmcov  35295  cvmcov2  35307  eldm3  35793  elima4  35808  neibastop1  36392  neibastop2lem  36393  neibastop2  36394  neibastop3  36395  neifg  36404  poimirlem17  37676  poimirlem18  37677  poimirlem20  37679  poimirlem21  37680  poimirlem22  37681  poimirlem23  37682  poimirlem27  37686  poimirlem28  37687  poimirlem30  37689  poimirlem31  37690  poimirlem32  37691  mblfinlem3  37698  itg2addnclem3  37712  sstotbnd2  37813  cntotbnd  37835  heibor1lem  37848  dmecd  38337  disjecxrn  38420  br1cosscnvxrn  38510  2llnm3N  39607  dalem4  39703  cdlemk28-3  40946  mapdh9a  41827  idomnnzpownz  42164  idomnnzgmulnz  42165  sticksstones1  42178  aks6d1c6lem1  42202  unitscyglem2  42228  unitscyglem3  42229  unitscyglem4  42230  readvcot  42396  domnexpgn0cl  42555  fsuppind  42622  dffltz  42666  pellexlem3  42863  mncn0  43171  aaitgo  43194  gneispace0nelrn2  44173  cvgdvgrat  44345  binomcxplemnotnn0  44388  disjf1  45219  disjrnmpt2  45224  disjinfi  45228  fsumiunss  45614  islptre  45658  islpcn  45676  lptre2pt  45677  0ellimcdiv  45686  liminflelimsup  45813  stoweidlem28  46065  stoweidlem43  46080  dirkercncflem2  46141  fourierdlem46  46189  fourierdlem79  46222  elaa2lem  46270  elaa2  46271  sge0fodjrnlem  46453  sge0iunmpt  46455  nnfoctbdjlem  46492  meadjiunlem  46502  meadjiun  46503  gpg5nbgrvtx13starlem1  48101  gpg5nbgrvtx13starlem3  48103  ovn0ssdmfun  48189  rmsupp0  48398  scmsuppss  48401  suppmptcfin  48406  linc1  48456  el0ldep  48497  ldepspr  48504  islindeps2  48514  zlmodzxzldeplem4  48534  zlmodzxzldep  48535  ldepsnlinclem1  48536  ldepsnlinclem2  48537  ldepsnlinc  48539  fvconstr  48892  fvconstrn0  48893  fvconstr2  48894  catprslem  49041  catprsc  49044  catprsc2  49045  oppccic  49075  relcic  49076  cicpropdlem  49080  secval  49778  cscval  49779  cotval  49780