Theorem necon3bid 2989

Description: Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypothesis

Ref	Expression
necon3bid.1	⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))

Assertion

Ref	Expression
necon3bid	⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))

Proof of Theorem necon3bid

Step	Hyp	Ref	Expression
1		df-ne 2945	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3bid.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))
3	2	necon3bbid 2982	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ 𝐶 ≠ 𝐷))
4	1, 3	bitrid 282	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   = wceq 1539   ≠ wne 2944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-ne 2945

This theorem is referenced by:  neeq1d  3004  neeq2d  3005  neeq12d  3006  nebi  3025  pr1nebg  4789  f1dom3fv3dif  7150  frxp  7976  suppval1  7992  iinon  8180  fodomfib  9102  wemapso  9319  wemapso2lem  9320  infpssrlem4  10071  ttukeylem6  10279  fodomb  10291  tskcard  10546  addneintrd  11191  addneintr2d  11192  negne0bd  11334  negned  11338  subne0d  11350  subne0ad  11352  subneintrd  11385  subneintr2d  11387  divne0b  11653  div2neg  11707  divne1d  11771  div2sub  11809  xaddass2  12993  xadddi2  13040  seqf1olem1  13771  expne0  13823  sqne0  13852  hashneq0  14088  hashnncl  14090  hashgt0  14112  ccat1st1st  14344  pfxn0  14408  cjne0  14883  recval  15043  absgt0  15045  abs1m  15056  abslem2  15060  sqreulem  15080  sqreu  15081  absne0d  15168  geoserg  15587  geolim  15591  geolim2  15592  georeclim  15593  geoisum1c  15601  tanval2  15851  tanaddlem  15884  tanadd  15885  4sqlem11  16665  ipodrsima  18268  f1omvdmvd  19060  f1omvdcnv  19061  f1omvdconj  19063  pmtrfmvdn0  19079  sylow1lem4  19215  dprdf1o  19644  dprd2da  19654  ringinvnz1ne0  19840  abvne0  20096  rrgsupp  20571  gzrngunit  20673  chrnzr  20743  obsne0  20941  mdetdiaglem  21756  cnhaus  22514  hauscmplem  22566  fsubbas  23027  metn0  23522  nmne0  23784  nmgt0  23795  iccpnfhmeo  24117  ncvs1  24330  ipcau2  24407  dvcnvlem  25149  dvlip  25166  ftc1lem5  25213  mdegldg  25240  ply1divmo  25309  ig1peu  25345  ig1pdvds  25350  dgrmul  25440  coecj  25448  plydivlem4  25465  vieta1lem2  25480  vieta1  25481  aareccl  25495  geolim3  25508  abelthlem2  25600  abelthlem7  25606  tanregt0  25704  tanarg  25783  logtayl  25824  abscxp2  25857  cxpsqrt  25867  abscxpbnd  25915  logrec  25922  ang180lem1  25968  ang180lem2  25969  ang180lem3  25970  lawcos  25975  isosctr  25980  asinlem  26027  atandm2  26036  atandm4  26038  2efiatan  26077  tanatan  26078  atandmtan  26079  dvatan  26094  mersenne  26384  perfectlem2  26387  dchrinv  26418  dchrptlem2  26422  dchrsum2  26425  sumdchr2  26427  lgsabs1  26493  dchrisum0re  26670  tgcgrneq  26853  footexALT  27088  footexlem1  27089  footexlem2  27090  colinearalg  27287  axsegconlem6  27299  axsegconlem9  27302  ax5seglem5  27310  axlowdimlem14  27332  wlkn0  27997  cyclnspth  28177  iswwlksnx  28214  wwlksm1edg  28255  wspthsnonn0vne  28291  umgrclwwlkge2  28364  clwwisshclwws  28388  hashecclwwlkn1  28450  umgrhashecclwwlk  28451  frgrregord013  28768  frgrogt3nreg  28770  friendshipgt3  28771  nvgt0  29045  nv1  29046  nmlnogt0  29168  nmblolbii  29170  blocnilem  29175  normne0  29501  normcan  29947  nmlnopne0  30370  nmophmi  30402  riesz3i  30433  ogrpsublt  31356  cycpmco2lem6  31407  zarclssn  31832  esumpcvgval  32055  ballotlemfrcn0  32505  signsply0  32539  signstfvn  32557  signsvtn0  32558  signstfvneq0  32560  signstfveq0a  32564  signshnz  32579  bnj168  32718  nummin  33072  usgrgt2cycl  33101  erdszelem9  33170  frxp2  33800  frxp3  33806  sltval2  33868  bday1s  34034  segcon2  34416  outsideofeu  34442  heicant  35821  smprngopr  36219  isfldidl2  36236  isdmn3  36241  lsat0cv  37054  lcvexchlem1  37055  lsatcvat2  37072  lkrshp  37126  lkrshp3  37127  lkrpssN  37184  cvrat2  37450  atcvrneN  37451  atcvrj2b  37453  2llnmat  37545  2lnat  37805  pmapjat1  37874  pclfinclN  37971  lautlt  38112  ltrn11at  38168  ltrnatneq  38203  trlcone  38749  tendoconid  38850  tendotr  38851  cdleml3N  38999  dochsordN  39395  dochn0nv  39396  djhcvat42  39436  dochsatshp  39472  lcfl8b  39525  lclkrlem2a  39528  lcfrlem9  39571  mapdsord  39676  mapdncol  39691  mapdpglem29  39721  mapdindp1  39741  hdmapnzcl  39866  hdmaprnlem1N  39870  hdmaprnlem3N  39871  hdmaprnlem3uN  39872  hdmaprnlem9N  39878  hdmap14lem9  39897  hgmapval1  39914  hgmapadd  39915  hgmapmul  39916  hgmaprnlem1N  39917  hdmaplkr  39934  hdmapip1  39937  hgmapvvlem1  39944  hgmapvvlem2  39945  hgmapvvlem3  39946  fsuppind  40286  jm2.19  40822  jm2.26lem3  40830  kelac1  40895  mpaaeu  40982  radcnvrat  41939  binomcxplemnotnn0  41981  sqrtnegnre  44810  paireqne  44974  fmtnoprmfac1lem  45027  requad01  45084  requad2  45086  perfectALTVlem2  45185  nnsgrpnmnd  45383  rrx2pnedifcoorneor  46073  rrx2pnedifcoorneorr  46074  eenglngeehlnmlem2  46095  fdomne0  46188  onetansqsecsq  46474