Theorem neeq1d 2999

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ≠ wne 2939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-ne 2940

This theorem is referenced by:  neeq1  3002  eqnetrd  3007  inisegn0  6055  f12dfv  7224  f13dfv  7225  suppval1  8103  elsuppfng  8106  elsuppfn  8107  suppsnop  8114  ressuppss  8119  ressuppssdif  8121  tz7.49  8396  ereldm  8703  pw2f1olem  9027  marypha1lem  9378  wdomtr  9520  inf3lem2  9574  cantnflem1  9634  cantnf  9638  cplem2  9835  dfac9  10081  kmlem12  10106  infpssrlem4  10251  fin23lem14  10278  axcc2lem  10381  axcc3  10383  domtriomlem  10387  axdc2lem  10393  ac6c4  10426  zorn2lem6  10446  rpnnen1lem4  12914  rpnnen1lem5  12915  mptnn0fsuppr  13914  hashprg  14305  hashtpg  14396  prodfn0  15790  prodfrec  15791  prodfdiv  15792  ntrivcvgtail  15796  fproddiv  15855  fprodn0  15873  fproddivf  15881  dvdsle  16203  algcvg  16463  algcvga  16466  eucalgcvga  16473  rpdvds  16547  phibndlem  16653  dfphi2  16657  pcaddlem  16771  vdwmc  16861  iscatd2  17575  brcic  17695  cicer  17703  cat1lem  17996  cat1  17997  sgrp2nmndlem5  18753  symgextf1lem  19216  pmtrmvd  19252  frgpup3lem  19573  isirred  20144  isdrngrd  20256  isdrngrdOLD  20258  rrgsupp  20798  dsmmelbas  21182  dsmmacl  21184  frlmssuvc2  21238  mhpsclcl  21574  mhpmulcl  21576  elcls  22461  clsndisj  22463  elcls3  22471  neindisj2  22511  clslp  22536  cmpfi  22796  cmpfii  22797  dfconn2  22807  connsuba  22808  nconnsubb  22811  1stcelcls  22849  finlocfin  22908  locfincmp  22914  dissnlocfin  22917  locfindis  22918  ptclsg  23003  dfac14lem  23005  isfbas  23217  trfbas2  23231  isfil  23235  filss  23241  fbunfip  23257  fgval  23258  elfg  23259  isufil2  23296  ufileu  23307  filufint  23308  fmfnfm  23346  flimclslem  23372  fclsopni  23403  fclsnei  23407  fclsbas  23409  fclsrest  23412  fclscmp  23418  ufilcmp  23420  isfcf  23422  fcfnei  23423  fcfneii  23425  ptcmplem2  23441  cnextcn  23455  cnextfres1  23456  tsmsfbas  23516  iscusp  23688  cuspcvg  23690  lpbl  23896  prdsxmslem2  23922  restmetu  23963  qdensere  24170  lebnumlem3  24363  isphtpc  24394  iscmet  24685  cmetcvg  24686  equivcmet  24718  cmetcusp1  24754  cmetcusp  24755  rrxmvallem  24805  ovolicc2lem2  24919  ovolicc2lem5  24922  i1fres  25107  lhop1lem  25414  deg1ldg  25494  plyco0  25590  plyeq0lem  25608  coeeq2  25640  coe1termlem  25656  taylfval  25755  cxpeq0  26070  ftalem4  26462  ftalem5  26463  ftalem6  26464  isppw  26500  isnsqf  26521  sqff1o  26568  musum  26577  dchrelbas3  26623  dchrelbasd  26624  dchrelbas4  26628  dchrmulcl  26634  dchrn0  26635  dchrfi  26640  dchrptlem2  26650  dchrpt  26652  lgsne0  26720  lgsdchr  26740  2sqlem11  26814  nosupbnd2lem1  27100  ishlg  27607  uvtx01vtx  28408  pthdlem2lem  28778  2pthdlem1  28938  clwwlknclwwlkdif  28986  umgr2cwwkdifex  29072  3pthdlem1  29171  frgrregorufr  29332  numclwwlk2lem1lem  29349  numclwwlk2lem1  29383  numclwlk2lem2f  29384  numclwlk2lem2f1o  29386  nmorepnf  29773  nmoprepnf  30872  nmfnrepnf  30885  ressupprn  31672  disjdsct  31684  rmfsupp2  32143  isufd  32336  fedgmullem2  32412  locfinreflem  32510  sibfof  33029  signswch  33262  signstfvneq0  33273  derangenlem  33852  subfacp1lem3  33863  subfacp1lem5  33865  subfacp1lem6  33866  subfacp1  33867  iscvm  33940  cvmcov  33944  cvmcov2  33956  eldm3  34420  elima4  34436  neibastop1  34907  neibastop2lem  34908  neibastop2  34909  neibastop3  34910  neifg  34919  poimirlem17  36168  poimirlem18  36169  poimirlem20  36171  poimirlem21  36172  poimirlem22  36173  poimirlem23  36174  poimirlem27  36178  poimirlem28  36179  poimirlem30  36181  poimirlem31  36182  poimirlem32  36183  mblfinlem3  36190  itg2addnclem3  36204  sstotbnd2  36306  cntotbnd  36328  heibor1lem  36341  dmecd  36838  disjecxrn  36924  br1cosscnvxrn  37009  2llnm3N  38105  dalem4  38201  cdlemk28-3  39444  mapdh9a  40325  sticksstones1  40627  metakunt29  40678  fsuppind  40823  dffltz  41030  pellexlem3  41212  mncn0  41524  aaitgo  41547  gneispace0nelrn2  42535  cvgdvgrat  42715  binomcxplemnotnn0  42758  disjf1  43523  disjrnmpt2  43529  disjinfi  43534  fsumiunss  43936  islptre  43980  islpcn  44000  lptre2pt  44001  0ellimcdiv  44010  liminflelimsup  44137  stoweidlem28  44389  stoweidlem43  44404  dirkercncflem2  44465  fourierdlem46  44513  fourierdlem79  44546  elaa2lem  44594  elaa2  44595  sge0fodjrnlem  44777  sge0iunmpt  44779  nnfoctbdjlem  44816  meadjiunlem  44826  meadjiun  44827  ovn0ssdmfun  46181  nzerooringczr  46490  rmsupp0  46564  scmsuppss  46568  suppmptcfin  46575  linc1  46626  el0ldep  46667  ldepspr  46674  islindeps2  46684  zlmodzxzldeplem4  46704  zlmodzxzldep  46705  ldepsnlinclem1  46706  ldepsnlinclem2  46707  ldepsnlinc  46709  fvconstr  47042  fvconstrn0  47043  fvconstr2  47044  catprslem  47150  catprsc  47153  catprsc2  47154  secval  47312  cscval  47313  cotval  47314