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  4485  inisegn0  6046  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  9783  dfac9  10028  kmlem12  10053  infpssrlem4  10197  fin23lem14  10224  axcc2lem  10327  axcc3  10329  domtriomlem  10333  axdc2lem  10339  ac6c4  10372  zorn2lem6  10392  rpnnen1lem4  12878  rpnnen1lem5  12879  mptnn0fsuppr  13906  hashprg  14302  hashtpg  14392  prodfn0  15801  prodfrec  15802  prodfdiv  15803  ntrivcvgtail  15807  fproddiv  15868  fprodn0  15886  fproddivf  15894  dvdsle  16221  algcvg  16487  algcvga  16490  eucalgcvga  16497  rpdvds  16571  phibndlem  16681  dfphi2  16685  pcaddlem  16800  vdwmc  16890  iscatd2  17587  brcic  17705  cicer  17713  cat1lem  18003  cat1  18004  sgrp2nmndlem5  18837  symgextf1lem  19332  pmtrmvd  19368  frgpup3lem  19689  isirred  20337  rrgsupp  20616  isdrngrd  20681  isdrngrdOLD  20683  nzerooringczr  21417  dsmmelbas  21676  dsmmacl  21678  frlmssuvc2  21732  mhpsclcl  22062  mhpmulcl  22064  elcls  22988  clsndisj  22990  elcls3  22998  neindisj2  23038  clslp  23063  cmpfi  23323  cmpfii  23324  dfconn2  23334  connsuba  23335  nconnsubb  23338  1stcelcls  23376  finlocfin  23435  locfincmp  23441  dissnlocfin  23444  locfindis  23445  ptclsg  23530  dfac14lem  23532  isfbas  23744  trfbas2  23758  isfil  23762  filss  23768  fbunfip  23784  fgval  23785  elfg  23786  isufil2  23823  ufileu  23834  filufint  23835  fmfnfm  23873  flimclslem  23899  fclsopni  23930  fclsnei  23934  fclsbas  23936  fclsrest  23939  fclscmp  23945  ufilcmp  23947  isfcf  23949  fcfnei  23950  fcfneii  23952  ptcmplem2  23968  cnextcn  23982  cnextfres1  23983  tsmsfbas  24043  iscusp  24213  cuspcvg  24215  lpbl  24418  prdsxmslem2  24444  restmetu  24485  qdensere  24684  lebnumlem3  24889  isphtpc  24920  iscmet  25211  cmetcvg  25212  equivcmet  25244  cmetcusp1  25280  cmetcusp  25281  rrxmvallem  25331  ovolicc2lem2  25446  ovolicc2lem5  25449  i1fres  25633  lhop1lem  25945  deg1ldg  26024  plyco0  26124  plyeq0lem  26142  coeeq2  26174  coe1termlem  26190  taylfval  26293  cxpeq0  26614  ftalem4  27013  ftalem5  27014  ftalem6  27015  isppw  27051  isnsqf  27072  sqff1o  27119  musum  27128  dchrelbas3  27176  dchrelbasd  27177  dchrelbas4  27181  dchrmulcl  27187  dchrn0  27188  dchrfi  27193  dchrptlem2  27203  dchrpt  27205  lgsne0  27273  lgsdchr  27293  2sqlem11  27367  nosupbnd2lem1  27654  expsne0  28359  ishlg  28580  uvtx01vtx  29375  pthdlem2lem  29745  2pthdlem1  29908  clwwlknclwwlkdif  29959  umgr2cwwkdifex  30045  3pthdlem1  30144  frgrregorufr  30305  numclwwlk2lem1lem  30322  numclwwlk2lem1  30356  numclwlk2lem2f  30357  numclwlk2lem2f1o  30359  nmorepnf  30748  nmoprepnf  31847  nmfnrepnf  31860  fdifsupp  32666  ressupprn  32671  disjdsct  32684  rmfsupp2  33205  domnprodn0  33242  isufd  33505  ufdprmidl  33506  1arithufdlem4  33512  dfufd2lem  33514  fedgmullem2  33643  constrconj  33758  constrelextdg2  33760  constrllcllem  33765  constrcbvlem  33768  locfinreflem  33853  sibfof  34353  signswch  34574  signstfvneq0  34585  vonf1owev  35152  derangenlem  35215  subfacp1lem3  35226  subfacp1lem5  35228  subfacp1lem6  35229  subfacp1  35230  iscvm  35303  cvmcov  35307  cvmcov2  35319  eldm3  35805  elima4  35820  neibastop1  36403  neibastop2lem  36404  neibastop2  36405  neibastop3  36406  neifg  36415  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  38341  disjecxrn  38435  br1cosscnvxrn  38575  2llnm3N  39667  dalem4  39763  cdlemk28-3  41006  mapdh9a  41887  idomnnzpownz  42224  idomnnzgmulnz  42225  sticksstones1  42238  aks6d1c6lem1  42262  unitscyglem2  42288  unitscyglem3  42289  unitscyglem4  42290  readvcot  42456  domnexpgn0cl  42615  fsuppind  42682  dffltz  42726  pellexlem3  42923  mncn0  43231  aaitgo  43254  gneispace0nelrn2  44233  cvgdvgrat  44405  binomcxplemnotnn0  44448  disjf1  45279  disjrnmpt2  45284  disjinfi  45288  fsumiunss  45674  islptre  45718  islpcn  45736  lptre2pt  45737  0ellimcdiv  45746  liminflelimsup  45873  stoweidlem28  46125  stoweidlem43  46140  dirkercncflem2  46201  fourierdlem46  46249  fourierdlem79  46282  elaa2lem  46330  elaa2  46331  sge0fodjrnlem  46513  sge0iunmpt  46515  nnfoctbdjlem  46552  meadjiunlem  46562  meadjiun  46563  gpg5nbgrvtx13starlem1  48170  gpg5nbgrvtx13starlem3  48172  ovn0ssdmfun  48258  rmsupp0  48467  scmsuppss  48470  suppmptcfin  48475  linc1  48525  el0ldep  48566  ldepspr  48573  islindeps2  48583  zlmodzxzldeplem4  48603  zlmodzxzldep  48604  ldepsnlinclem1  48605  ldepsnlinclem2  48606  ldepsnlinc  48608  fvconstr  48961  fvconstrn0  48962  fvconstr2  48963  catprslem  49110  catprsc  49113  catprsc2  49114  oppccic  49144  relcic  49145  cicpropdlem  49149  secval  49847  cscval  49848  cotval  49849