Theorem neeq1d 3014

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ne 2956

This theorem is used by:  neeq1  3017  eqnetrd  3022  iftrueb  4494  inisegn0  6095  f1ounsn  7280  f12dfv  7281  f13dfv  7282  ovn0ssdmfun  7589  resf1extb  7946  suppval1  8186  elsuppfng  8189  elsuppfn  8190  suppsnop  8198  ressuppss  8203  ressuppssdif  8205  tz7.49  8458  ereldm  8774  pw2f1olem  9103  marypha1lem  9428  wdomtr  9572  inf3lem2  9633  cantnflem1  9693  cantnf  9697  cplem2  9955  cplem2OLD  9956  dfac9  10218  kmlem12  10243  infpssrlem4  10387  fin23lem14  10414  axcc2lem  10517  axcc3  10519  domtriomlem  10523  axdc2lem  10529  ac6c4  10562  zorn2lem6  10582  rpnnen1lem4  13111  rpnnen1lem5  13112  mptnn0fsuppr  14145  hashprg  14542  hashtpg  14633  prodfn0  16068  prodfrec  16069  prodfdiv  16070  ntrivcvgtail  16074  fproddiv  16133  fprodn0  16151  fproddivf  16159  dvdsle  16485  algcvg  16756  algcvga  16759  eucalgcvga  16766  rpdvds  16840  phibndlem  16952  dfphi2  16956  pcaddlem  17071  vdwmc  17161  iscatd2  17860  brcic  17978  cicer  17986  cat1lem  18276  cat1  18277  sgrp2nmndlem5  19133  symgextf1lem  19639  pmtrmvd  19675  frgpup3lem  19996  isirred  20654  rrgsupp  20958  isdrngrd  21028  isdrngrdOLD  21030  nzerooringczr  21791  dsmmelbas  22050  dsmmacl  22052  frlmssuvc2  22106  mhpsclcl  22473  mhpmulcl  22475  elcls  23396  clsndisj  23398  elcls3  23406  neindisj2  23446  clslp  23471  cmpfi  23731  cmpfii  23732  dfconn2  23742  connsuba  23743  nconnsubb  23746  1stcelcls  23785  finlocfin  23844  locfincmp  23850  dissnlocfin  23853  locfindis  23854  ptclsg  23939  dfac14lem  23941  isfbas  24153  trfbas2  24167  isfil  24171  filss  24177  fbunfip  24193  fgval  24194  elfg  24195  isufil2  24232  ufileu  24243  filufint  24244  fmfnfm  24282  flimclslem  24308  fclsopni  24339  fclsnei  24343  fclsbas  24345  fclsrest  24348  fclscmp  24354  ufilcmp  24356  isfcf  24358  fcfnei  24359  fcfneii  24361  ptcmplem2  24377  cnextcn  24391  cnextfres1  24392  tsmsfbas  24452  iscusp  24622  cuspcvg  24624  lpbl  24827  prdsxmslem2  24853  restmetu  24894  qdensere  25093  lebnumlem3  25289  isphtpc  25320  iscmet  25610  cmetcvg  25611  equivcmet  25643  cmetcusp1  25679  cmetcusp  25680  rrxmvallem  25730  ovolicc2lem2  25844  ovolicc2lem5  25847  i1fres  26031  lhop1lem  26338  deg1ldg  26415  plyco0  26515  plyeq0lem  26534  coeeq2  26566  coe1termlem  26582  rnplynfin  26635  plyconz  26636  taylfval  26691  cxpeq0  27011  ftalem4  27408  ftalem5  27409  ftalem6  27410  isppw  27446  isnsqf  27467  sqff1o  27514  musum  27523  dchrelbas3  27570  dchrelbasd  27571  dchrelbas4  27575  dchrmulcl  27581  dchrn0  27582  dchrfi  27587  dchrptlem2  27597  dchrpt  27599  lgsne0  27667  lgsdchr  27687  2sqlem11  27761  flt4ALT  27997  fltoprm  28000  nosupbnd2lem1  28077  expsne0  28827  ishlg2  29070  ishlg  29073  elcgrabasi  29380  angmgmaddov1  29393  angmgmaddcpbl  29395  angmgmaddcl  29396  angmgmval  29399  uvtx01vtx  29983  pthdlem2lem  30358  2pthdlem1  30524  clwwlknclwwlkdif  30575  umgr2cwwkdifex  30661  3pthdlem1  30770  frgrregorufr  30931  numclwwlk2lem1lem  30948  numclwwlk2lem1  30982  numclwlk2lem2f  30983  numclwlk2lem2f1o  30985  nmorepnf  31375  nmoprepnf  32474  nmfnrepnf  32487  fdifsupp  33325  ressupprn  33330  disjdsct  33343  suppgsumssiun  33679  rmfsupp2  33844  domnprodn0  33885  isufd  34118  ufdprmidl  34119  1arithufdlem4  34125  dfufd2lem  34127  fedgmullem2  34308  constrconj  34423  constrelextdg2  34425  constrllcllem  34430  constrcbvlem  34433  locfinreflem  34518  sibfof  35018  signswch  35236  signstfvneq0  35247  vonf1wev  35955  vonf1owevOLD  35957  derangenlem  36022  subfacp1lem3  36033  subfacp1lem5  36035  subfacp1lem6  36036  subfacp1  36037  iscvm  36110  cvmcov  36114  cvmcov2  36126  eldm3  36618  elima4  36632  neibastop1  37239  neibastop2lem  37240  neibastop2  37241  neibastop3  37242  neifg  37251  dfttc4lem1  37408  dfttc4lem2  37409  mh-inf3f1  37421  poimirlem17  38648  poimirlem18  38649  poimirlem20  38651  poimirlem21  38652  poimirlem22  38653  poimirlem23  38654  poimirlem27  38658  poimirlem28  38659  poimirlem30  38661  poimirlem31  38662  poimirlem32  38663  mblfinlem3  38670  itg2addnclem3  38684  sstotbnd2  38801  cntotbnd  38823  heibor1lem  38836  dmecd  39335  disjecxrn  39437  br1cosscnvxrn  39589  disjimeceqim  39829  eldisjim3  39840  2llnm3N  40719  dalem4  40815  cdlemk28-3  42058  mapdh9a  42939  idomnnzpownz  43275  idomnnzgmulnz  43276  sticksstones1  43289  aks6d1c6lem1  43313  unitscyglem2  43339  unitscyglem3  43340  unitscyglem4  43341  readvcot  43508  domnexpgn0cl  43677  fsuppind  43711  frlmnzcoordval  43746  frlmnzcoordn0  43750  dffltz  43763  pellexlem3  43931  mncn0  44234  aaitgo  44257  gneispace0nelrn2  45234  cvgdvgrat  45390  binomcxplemnotnn0  45433  disjf1  46291  disjrnmpt2  46296  disjinfi  46300  fsumiunss  46680  islptre  46724  islpcn  46742  lptre2pt  46743  0ellimcdiv  46752  liminflelimsup  46879  stoweidlem28  47131  stoweidlem43  47146  dirkercncflem2  47207  fourierdlem46  47255  fourierdlem79  47288  elaa2lem  47336  elaa2  47337  sge0fodjrnlem  47519  sge0iunmpt  47521  nnfoctbdjlem  47558  meadjiunlem  47568  meadjiun  47569  gpg5nbgrvtx13starlem1  49262  gpg5nbgrvtx13starlem3  49264  rmsupp0  49573  scmsuppss  49576  suppmptcfin  49581  linc1  49630  el0ldep  49671  ldepspr  49678  islindeps2  49688  zlmodzxzldeplem4  49708  zlmodzxzldep  49709  ldepsnlinclem1  49710  ldepsnlinclem2  49711  ldepsnlinc  49713  ovconstbrd  50066  ovconstbrn0d  50067  elovconstbrd  50068  catprslem  50217  catprsc  50220  catprsc2  50221  oppccic  50251  relcic  50252  cicpropdlem  50256  secval  51008  cscval  51009  cotval  51010  dvsec  51024  dvcsc  51025  dvcot  51026