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 1541   ≠ wne 2932

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 2123  ax-ext 2708

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

This theorem is referenced by:  neeq1  2994  eqnetrd  2999  iftrueb  4492  inisegn0  6057  f1ounsn  7218  f12dfv  7219  f13dfv  7220  resf1extb  7876  suppval1  8108  elsuppfng  8111  elsuppfn  8112  suppsnop  8120  ressuppss  8125  ressuppssdif  8127  tz7.49  8376  ereldm  8688  pw2f1olem  9009  marypha1lem  9336  wdomtr  9480  inf3lem2  9538  cantnflem1  9598  cantnf  9602  cplem2  9802  dfac9  10047  kmlem12  10072  infpssrlem4  10216  fin23lem14  10243  axcc2lem  10346  axcc3  10348  domtriomlem  10352  axdc2lem  10358  ac6c4  10391  zorn2lem6  10411  rpnnen1lem4  12893  rpnnen1lem5  12894  mptnn0fsuppr  13922  hashprg  14318  hashtpg  14408  prodfn0  15817  prodfrec  15818  prodfdiv  15819  ntrivcvgtail  15823  fproddiv  15884  fprodn0  15902  fproddivf  15910  dvdsle  16237  algcvg  16503  algcvga  16506  eucalgcvga  16513  rpdvds  16587  phibndlem  16697  dfphi2  16701  pcaddlem  16816  vdwmc  16906  iscatd2  17604  brcic  17722  cicer  17730  cat1lem  18020  cat1  18021  sgrp2nmndlem5  18854  symgextf1lem  19349  pmtrmvd  19385  frgpup3lem  19706  isirred  20355  rrgsupp  20634  isdrngrd  20699  isdrngrdOLD  20701  nzerooringczr  21435  dsmmelbas  21694  dsmmacl  21696  frlmssuvc2  21750  mhpsclcl  22090  mhpmulcl  22092  elcls  23017  clsndisj  23019  elcls3  23027  neindisj2  23067  clslp  23092  cmpfi  23352  cmpfii  23353  dfconn2  23363  connsuba  23364  nconnsubb  23367  1stcelcls  23405  finlocfin  23464  locfincmp  23470  dissnlocfin  23473  locfindis  23474  ptclsg  23559  dfac14lem  23561  isfbas  23773  trfbas2  23787  isfil  23791  filss  23797  fbunfip  23813  fgval  23814  elfg  23815  isufil2  23852  ufileu  23863  filufint  23864  fmfnfm  23902  flimclslem  23928  fclsopni  23959  fclsnei  23963  fclsbas  23965  fclsrest  23968  fclscmp  23974  ufilcmp  23976  isfcf  23978  fcfnei  23979  fcfneii  23981  ptcmplem2  23997  cnextcn  24011  cnextfres1  24012  tsmsfbas  24072  iscusp  24242  cuspcvg  24244  lpbl  24447  prdsxmslem2  24473  restmetu  24514  qdensere  24713  lebnumlem3  24918  isphtpc  24949  iscmet  25240  cmetcvg  25241  equivcmet  25273  cmetcusp1  25309  cmetcusp  25310  rrxmvallem  25360  ovolicc2lem2  25475  ovolicc2lem5  25478  i1fres  25662  lhop1lem  25974  deg1ldg  26053  plyco0  26153  plyeq0lem  26171  coeeq2  26203  coe1termlem  26219  taylfval  26322  cxpeq0  26643  ftalem4  27042  ftalem5  27043  ftalem6  27044  isppw  27080  isnsqf  27101  sqff1o  27148  musum  27157  dchrelbas3  27205  dchrelbasd  27206  dchrelbas4  27210  dchrmulcl  27216  dchrn0  27217  dchrfi  27222  dchrptlem2  27232  dchrpt  27234  lgsne0  27302  lgsdchr  27322  2sqlem11  27396  nosupbnd2lem1  27683  expsne0  28432  ishlg  28674  uvtx01vtx  29470  pthdlem2lem  29840  2pthdlem1  30003  clwwlknclwwlkdif  30054  umgr2cwwkdifex  30140  3pthdlem1  30239  frgrregorufr  30400  numclwwlk2lem1lem  30417  numclwwlk2lem1  30451  numclwlk2lem2f  30452  numclwlk2lem2f1o  30454  nmorepnf  30843  nmoprepnf  31942  nmfnrepnf  31955  fdifsupp  32764  ressupprn  32769  disjdsct  32782  rmfsupp2  33320  domnprodn0  33357  isufd  33621  ufdprmidl  33622  1arithufdlem4  33628  dfufd2lem  33630  fedgmullem2  33787  constrconj  33902  constrelextdg2  33904  constrllcllem  33909  constrcbvlem  33912  locfinreflem  33997  sibfof  34497  signswch  34718  signstfvneq0  34729  vonf1owev  35302  derangenlem  35365  subfacp1lem3  35376  subfacp1lem5  35378  subfacp1lem6  35379  subfacp1  35380  iscvm  35453  cvmcov  35457  cvmcov2  35469  eldm3  35955  elima4  35970  neibastop1  36553  neibastop2lem  36554  neibastop2  36555  neibastop3  36556  neifg  36565  poimirlem17  37834  poimirlem18  37835  poimirlem20  37837  poimirlem21  37838  poimirlem22  37839  poimirlem23  37840  poimirlem27  37844  poimirlem28  37845  poimirlem30  37847  poimirlem31  37848  poimirlem32  37849  mblfinlem3  37856  itg2addnclem3  37870  sstotbnd2  37971  cntotbnd  37993  heibor1lem  38006  dmecd  38499  disjecxrn  38593  br1cosscnvxrn  38733  2llnm3N  39825  dalem4  39921  cdlemk28-3  41164  mapdh9a  42045  idomnnzpownz  42382  idomnnzgmulnz  42383  sticksstones1  42396  aks6d1c6lem1  42420  unitscyglem2  42446  unitscyglem3  42447  unitscyglem4  42448  readvcot  42615  domnexpgn0cl  42774  fsuppind  42829  dffltz  42873  pellexlem3  43069  mncn0  43377  aaitgo  43400  gneispace0nelrn2  44378  cvgdvgrat  44550  binomcxplemnotnn0  44593  disjf1  45423  disjrnmpt2  45428  disjinfi  45432  fsumiunss  45817  islptre  45861  islpcn  45879  lptre2pt  45880  0ellimcdiv  45889  liminflelimsup  46016  stoweidlem28  46268  stoweidlem43  46283  dirkercncflem2  46344  fourierdlem46  46392  fourierdlem79  46425  elaa2lem  46473  elaa2  46474  sge0fodjrnlem  46656  sge0iunmpt  46658  nnfoctbdjlem  46695  meadjiunlem  46705  meadjiun  46706  gpg5nbgrvtx13starlem1  48313  gpg5nbgrvtx13starlem3  48315  ovn0ssdmfun  48401  rmsupp0  48610  scmsuppss  48613  suppmptcfin  48618  linc1  48667  el0ldep  48708  ldepspr  48715  islindeps2  48725  zlmodzxzldeplem4  48745  zlmodzxzldep  48746  ldepsnlinclem1  48747  ldepsnlinclem2  48748  ldepsnlinc  48750  fvconstr  49103  fvconstrn0  49104  fvconstr2  49105  catprslem  49251  catprsc  49254  catprsc2  49255  oppccic  49285  relcic  49286  cicpropdlem  49290  secval  49988  cscval  49989  cotval  49990