Theorem neeq1d 2994

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ≠ wne 2935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ne 2936

This theorem is referenced by:  neeq1  2997  eqnetrd  3002  iftrueb  4474  inisegn0  6057  f1ounsn  7223  f12dfv  7224  f13dfv  7225  resf1extb  7881  suppval1  8113  elsuppfng  8116  elsuppfn  8117  suppsnop  8125  ressuppss  8130  ressuppssdif  8132  tz7.49  8381  ereldm  8694  pw2f1olem  9016  marypha1lem  9343  wdomtr  9487  inf3lem2  9548  cantnflem1  9608  cantnf  9612  cplem2  9812  dfac9  10057  kmlem12  10082  infpssrlem4  10226  fin23lem14  10253  axcc2lem  10356  axcc3  10358  domtriomlem  10362  axdc2lem  10368  ac6c4  10401  zorn2lem6  10421  rpnnen1lem4  12928  rpnnen1lem5  12929  mptnn0fsuppr  13959  hashprg  14355  hashtpg  14445  prodfn0  15857  prodfrec  15858  prodfdiv  15859  ntrivcvgtail  15863  fproddiv  15924  fprodn0  15942  fproddivf  15950  dvdsle  16277  algcvg  16543  algcvga  16546  eucalgcvga  16553  rpdvds  16627  phibndlem  16738  dfphi2  16742  pcaddlem  16857  vdwmc  16947  iscatd2  17645  brcic  17763  cicer  17771  cat1lem  18061  cat1  18062  sgrp2nmndlem5  18898  symgextf1lem  19393  pmtrmvd  19429  frgpup3lem  19750  isirred  20397  rrgsupp  20680  isdrngrd  20745  isdrngrdOLD  20747  nzerooringczr  21462  dsmmelbas  21721  dsmmacl  21723  frlmssuvc2  21777  mhpsclcl  22142  mhpmulcl  22144  elcls  23063  clsndisj  23065  elcls3  23073  neindisj2  23113  clslp  23138  cmpfi  23398  cmpfii  23399  dfconn2  23409  connsuba  23410  nconnsubb  23413  1stcelcls  23451  finlocfin  23510  locfincmp  23516  dissnlocfin  23519  locfindis  23520  ptclsg  23605  dfac14lem  23607  isfbas  23819  trfbas2  23833  isfil  23837  filss  23843  fbunfip  23859  fgval  23860  elfg  23861  isufil2  23898  ufileu  23909  filufint  23910  fmfnfm  23948  flimclslem  23974  fclsopni  24005  fclsnei  24009  fclsbas  24011  fclsrest  24014  fclscmp  24020  ufilcmp  24022  isfcf  24024  fcfnei  24025  fcfneii  24027  ptcmplem2  24043  cnextcn  24057  cnextfres1  24058  tsmsfbas  24118  iscusp  24288  cuspcvg  24290  lpbl  24493  prdsxmslem2  24519  restmetu  24560  qdensere  24759  lebnumlem3  24955  isphtpc  24986  iscmet  25276  cmetcvg  25277  equivcmet  25309  cmetcusp1  25345  cmetcusp  25346  rrxmvallem  25396  ovolicc2lem2  25510  ovolicc2lem5  25513  i1fres  25697  lhop1lem  26005  deg1ldg  26082  plyco0  26182  plyeq0lem  26200  coeeq2  26232  coe1termlem  26248  taylfval  26349  cxpeq0  26667  ftalem4  27064  ftalem5  27065  ftalem6  27066  isppw  27102  isnsqf  27123  sqff1o  27170  musum  27179  dchrelbas3  27226  dchrelbasd  27227  dchrelbas4  27231  dchrmulcl  27237  dchrn0  27238  dchrfi  27243  dchrptlem2  27253  dchrpt  27255  lgsne0  27323  lgsdchr  27343  2sqlem11  27417  nosupbnd2lem1  27704  expsne0  28453  ishlg  28695  uvtx01vtx  29491  pthdlem2lem  29860  2pthdlem1  30023  clwwlknclwwlkdif  30074  umgr2cwwkdifex  30160  3pthdlem1  30259  frgrregorufr  30420  numclwwlk2lem1lem  30437  numclwwlk2lem1  30471  numclwlk2lem2f  30472  numclwlk2lem2f1o  30474  nmorepnf  30864  nmoprepnf  31963  nmfnrepnf  31976  fdifsupp  32784  ressupprn  32789  disjdsct  32802  suppgsumssiun  33160  rmfsupp2  33326  domnprodn0  33363  isufd  33630  ufdprmidl  33631  1arithufdlem4  33637  dfufd2lem  33639  fedgmullem2  33821  constrconj  33936  constrelextdg2  33938  constrllcllem  33943  constrcbvlem  33946  locfinreflem  34031  sibfof  34531  signswch  34752  signstfvneq0  34763  vonf1owev  35343  derangenlem  35406  subfacp1lem3  35417  subfacp1lem5  35419  subfacp1lem6  35420  subfacp1  35421  iscvm  35494  cvmcov  35498  cvmcov2  35510  eldm3  35996  elima4  36011  neibastop1  36594  neibastop2lem  36595  neibastop2  36596  neibastop3  36597  neifg  36606  dfttc4lem1  36763  dfttc4lem2  36764  poimirlem17  38011  poimirlem18  38012  poimirlem20  38014  poimirlem21  38015  poimirlem22  38016  poimirlem23  38017  poimirlem27  38021  poimirlem28  38022  poimirlem30  38024  poimirlem31  38025  poimirlem32  38026  mblfinlem3  38033  itg2addnclem3  38047  sstotbnd2  38148  cntotbnd  38170  heibor1lem  38183  dmecd  38684  disjecxrn  38786  br1cosscnvxrn  38938  disjimeceqim  39178  eldisjim3  39189  2llnm3N  40068  dalem4  40164  cdlemk28-3  41407  mapdh9a  42288  idomnnzpownz  42624  idomnnzgmulnz  42625  sticksstones1  42638  aks6d1c6lem1  42662  unitscyglem2  42688  unitscyglem3  42689  unitscyglem4  42690  readvcot  42848  domnexpgn0cl  43016  fsuppind  43047  dffltz  43091  pellexlem3  43283  mncn0  43591  aaitgo  43614  gneispace0nelrn2  44592  cvgdvgrat  44764  binomcxplemnotnn0  44807  disjf1  45637  disjrnmpt2  45642  disjinfi  45646  fsumiunss  46027  islptre  46071  islpcn  46089  lptre2pt  46090  0ellimcdiv  46099  liminflelimsup  46226  stoweidlem28  46478  stoweidlem43  46493  dirkercncflem2  46554  fourierdlem46  46602  fourierdlem79  46635  elaa2lem  46683  elaa2  46684  sge0fodjrnlem  46866  sge0iunmpt  46868  nnfoctbdjlem  46905  meadjiunlem  46915  meadjiun  46916  gpg5nbgrvtx13starlem1  48569  gpg5nbgrvtx13starlem3  48571  ovn0ssdmfun  48657  rmsupp0  48866  scmsuppss  48869  suppmptcfin  48874  linc1  48923  el0ldep  48964  ldepspr  48971  islindeps2  48981  zlmodzxzldeplem4  49001  zlmodzxzldep  49002  ldepsnlinclem1  49003  ldepsnlinclem2  49004  ldepsnlinc  49006  fvconstr  49359  fvconstrn0  49360  fvconstr2  49361  catprslem  49507  catprsc  49510  catprsc2  49511  oppccic  49541  relcic  49542  cicpropdlem  49546  secval  50244  cscval  50245  cotval  50246