Theorem neeq1d 2998

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 2983	1 ⊢ (𝜑 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ≠ wne 2938

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-ne 2939

This theorem is referenced by:  neeq1  3001  eqnetrd  3006  inisegn0  6098  f12dfv  7275  f13dfv  7276  suppval1  8156  elsuppfng  8159  elsuppfn  8160  suppsnop  8167  ressuppss  8172  ressuppssdif  8174  tz7.49  8449  ereldm  8755  pw2f1olem  9080  marypha1lem  9432  wdomtr  9574  inf3lem2  9628  cantnflem1  9688  cantnf  9692  cplem2  9889  dfac9  10135  kmlem12  10160  infpssrlem4  10305  fin23lem14  10332  axcc2lem  10435  axcc3  10437  domtriomlem  10441  axdc2lem  10447  ac6c4  10480  zorn2lem6  10500  rpnnen1lem4  12970  rpnnen1lem5  12971  mptnn0fsuppr  13970  hashprg  14361  hashtpg  14452  prodfn0  15846  prodfrec  15847  prodfdiv  15848  ntrivcvgtail  15852  fproddiv  15911  fprodn0  15929  fproddivf  15937  dvdsle  16259  algcvg  16519  algcvga  16522  eucalgcvga  16529  rpdvds  16603  phibndlem  16709  dfphi2  16713  pcaddlem  16827  vdwmc  16917  iscatd2  17631  brcic  17751  cicer  17759  cat1lem  18052  cat1  18053  sgrp2nmndlem5  18848  symgextf1lem  19331  pmtrmvd  19367  frgpup3lem  19688  isirred  20312  isdrngrd  20536  isdrngrdOLD  20538  rrgsupp  21109  dsmmelbas  21515  dsmmacl  21517  frlmssuvc2  21571  mhpsclcl  21911  mhpmulcl  21913  elcls  22799  clsndisj  22801  elcls3  22809  neindisj2  22849  clslp  22874  cmpfi  23134  cmpfii  23135  dfconn2  23145  connsuba  23146  nconnsubb  23149  1stcelcls  23187  finlocfin  23246  locfincmp  23252  dissnlocfin  23255  locfindis  23256  ptclsg  23341  dfac14lem  23343  isfbas  23555  trfbas2  23569  isfil  23573  filss  23579  fbunfip  23595  fgval  23596  elfg  23597  isufil2  23634  ufileu  23645  filufint  23646  fmfnfm  23684  flimclslem  23710  fclsopni  23741  fclsnei  23745  fclsbas  23747  fclsrest  23750  fclscmp  23756  ufilcmp  23758  isfcf  23760  fcfnei  23761  fcfneii  23763  ptcmplem2  23779  cnextcn  23793  cnextfres1  23794  tsmsfbas  23854  iscusp  24026  cuspcvg  24028  lpbl  24234  prdsxmslem2  24260  restmetu  24301  qdensere  24508  lebnumlem3  24711  isphtpc  24742  iscmet  25034  cmetcvg  25035  equivcmet  25067  cmetcusp1  25103  cmetcusp  25104  rrxmvallem  25154  ovolicc2lem2  25269  ovolicc2lem5  25272  i1fres  25457  lhop1lem  25764  deg1ldg  25844  plyco0  25940  plyeq0lem  25958  coeeq2  25990  coe1termlem  26006  taylfval  26105  cxpeq0  26420  ftalem4  26814  ftalem5  26815  ftalem6  26816  isppw  26852  isnsqf  26873  sqff1o  26920  musum  26929  dchrelbas3  26975  dchrelbasd  26976  dchrelbas4  26980  dchrmulcl  26986  dchrn0  26987  dchrfi  26992  dchrptlem2  27002  dchrpt  27004  lgsne0  27072  lgsdchr  27092  2sqlem11  27166  nosupbnd2lem1  27452  ishlg  28118  uvtx01vtx  28919  pthdlem2lem  29289  2pthdlem1  29449  clwwlknclwwlkdif  29497  umgr2cwwkdifex  29583  3pthdlem1  29682  frgrregorufr  29843  numclwwlk2lem1lem  29860  numclwwlk2lem1  29894  numclwlk2lem2f  29895  numclwlk2lem2f1o  29897  nmorepnf  30286  nmoprepnf  31385  nmfnrepnf  31398  ressupprn  32177  disjdsct  32189  rmfsupp2  32655  isufd  32904  fedgmullem2  33001  locfinreflem  33116  sibfof  33635  signswch  33868  signstfvneq0  33879  derangenlem  34458  subfacp1lem3  34469  subfacp1lem5  34471  subfacp1lem6  34472  subfacp1  34473  iscvm  34546  cvmcov  34550  cvmcov2  34562  eldm3  35033  elima4  35049  neibastop1  35549  neibastop2lem  35550  neibastop2  35551  neibastop3  35552  neifg  35561  poimirlem17  36810  poimirlem18  36811  poimirlem20  36813  poimirlem21  36814  poimirlem22  36815  poimirlem23  36816  poimirlem27  36820  poimirlem28  36821  poimirlem30  36823  poimirlem31  36824  poimirlem32  36825  mblfinlem3  36832  itg2addnclem3  36846  sstotbnd2  36947  cntotbnd  36969  heibor1lem  36982  dmecd  37478  disjecxrn  37564  br1cosscnvxrn  37649  2llnm3N  38745  dalem4  38841  cdlemk28-3  40084  mapdh9a  40965  sticksstones1  41270  metakunt29  41321  fsuppind  41466  dffltz  41680  pellexlem3  41873  mncn0  42185  aaitgo  42208  gneispace0nelrn2  43196  cvgdvgrat  43376  binomcxplemnotnn0  43419  disjf1  44182  disjrnmpt2  44187  disjinfi  44191  fsumiunss  44591  islptre  44635  islpcn  44655  lptre2pt  44656  0ellimcdiv  44665  liminflelimsup  44792  stoweidlem28  45044  stoweidlem43  45059  dirkercncflem2  45120  fourierdlem46  45168  fourierdlem79  45201  elaa2lem  45249  elaa2  45250  sge0fodjrnlem  45432  sge0iunmpt  45434  nnfoctbdjlem  45471  meadjiunlem  45481  meadjiun  45482  ovn0ssdmfun  46837  nzerooringczr  47060  rmsupp0  47134  scmsuppss  47138  suppmptcfin  47145  linc1  47195  el0ldep  47236  ldepspr  47243  islindeps2  47253  zlmodzxzldeplem4  47273  zlmodzxzldep  47274  ldepsnlinclem1  47275  ldepsnlinclem2  47276  ldepsnlinc  47278  fvconstr  47611  fvconstrn0  47612  fvconstr2  47613  catprslem  47719  catprsc  47722  catprsc2  47723  secval  47881  cscval  47882  cotval  47883