Theorem necon3bid 3000

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 2957	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3bid.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))
3	2	necon3bbid 2993	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ 𝐶 ≠ 𝐷))
4	1, 3	bitrid 286	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2957

This theorem is used by:  neeq1d  3015  neeq2d  3016  neeq12d  3017  nebi  3036  pr1nebg  4818  f1dom3fv3dif  7272  frxp  8138  fnwe2lem3  8147  frxp2  8161  frxp3  8168  suppval1  8183  iinon  8348  onelfvnef1  8449  fodomfib  9320  wemapso  9545  wemapso2lem  9546  infpssrlem4  10384  ttukeylem6  10592  fodomb  10605  tskcard  10866  addneintrd  11517  addneintr2d  11518  negne0bd  11662  negned  11666  subne0d  11679  subne0ad  11680  subneintrd  11713  subneintr2d  11715  divne0b  11985  div2neg  12040  divne1d  12104  div2sub  12142  xaddass2  13380  xadddi2  13427  seqf1olem1  14184  expne0  14236  sqne0  14266  hashneq0  14508  hashnncl  14510  hashgt0  14532  ccat1st1st  14776  pfxn0  14836  cjne0  15330  recval  15490  absgt0  15492  abs1m  15503  abslem2  15507  sqreulem  15527  sqreu  15528  absne0d  15617  geoserg  16035  geolim  16039  geolim2  16040  georeclim  16041  geoisum1c  16049  tanval2  16301  tanaddlem  16334  tanadd  16335  4sqlem11  17133  ipodrsima  18715  chnind  18795  chnub  18796  f1omvdmvd  19657  f1omvdcnv  19658  f1omvdconj  19660  pmtrfmvdn0  19676  sylow1lem4  19815  dprdf1o  20248  dprd2da  20258  ogrpsublt  20356  ringinvnz1ne0  20531  rrgsupp  20953  abvne0  21076  isfieldidl2  21541  gzrngunit  21739  chrnzr  21836  obsne0  22031  mdetdiaglem  22913  cnhaus  23672  hauscmplem  23724  fsubbas  24186  metn0  24679  nmne0  24938  nmgt0  24949  iccpnfhmeo  25266  ncvs1  25478  ipcau2  25555  dvcnvlem  26296  dvlip  26313  ftc1lem5  26360  mdegldg  26384  ply1divmo  26454  ig1peu  26493  ig1pdvds  26498  dgrmul  26589  coecj  26597  plydivlem4  26617  rnplynfin  26630  vieta1lem2  26634  vieta1  26635  aareccl  26653  geolim3  26666  abelthlem2  26759  abelthlem7  26765  tanregt0  26867  tanarg  26947  logtayl  26988  abscxp2  27021  cxpsqrt  27031  abscxpbnd  27081  logrec  27091  ang180lem1  27137  ang180lem2  27138  ang180lem3  27139  lawcos  27144  isosctr  27149  asinlem  27196  atandm2  27205  atandm4  27207  2efiatan  27246  tanatan  27247  atandmtan  27248  dvatan  27263  mersenne  27554  perfectlem2  27557  dchrinv  27588  dchrptlem2  27592  dchrsum2  27595  sumdchr2  27597  lgsabs1  27663  dchrisum0re  27840  ltsval2  28013  bday1  28200  cuteq1  28203  n0subs2  28750  tgcgrneq  28945  mirlni  29167  footexALT  29193  footexlem1  29194  footexlem2  29195  prlngsymquadlem  29441  colinearalg  29488  axsegconlem6  29500  axsegconlem9  29503  ax5seglem5  29511  axlowdimlem14  29533  wlkn0  30201  cyclnspth  30389  iswwlksnx  30429  wwlksm1edg  30470  wspthsnonn0vne  30506  umgrclwwlkge2  30582  clwwisshclwws  30606  hashecclwwlkn1  30668  umgrhashecclwwlk  30669  frgrregord013  30996  frgrogt3nreg  30998  friendshipgt3  30999  nrt2irr  31074  nvgt0  31276  nv1  31277  nmlnogt0  31399  nmblolbii  31401  blocnilem  31406  normne0  31732  normcan  32178  nmlnopne0  32601  nmophmi  32633  riesz3i  32664  hashne0  33401  wrdpmtrlast  33654  cycpmco2lem6  33692  1arithidom  34069  ply1unit  34107  m1pmeq  34117  minplyirredlem  34342  constrrtcclem  34366  constrconj  34377  iconstr  34398  zarclssn  34505  esumpcvgval  34710  ballotlemfrcn0  35162  signsply0  35180  signstfvn  35198  signsvtn0  35199  signstfvneq0  35201  signstfveq0a  35205  signshnz  35220  bnj168  35361  nummin  35722  usgrgt2cycl  35909  erdszelem9  35964  segcon2  36870  outsideofeu  36896  mh-inf3f1  37329  heicant  38573  smprngopr  38986  isfldidl2  39003  isdmn3  39008  lsat0cv  40090  lcvexchlem1  40091  lsatcvat2  40108  lkrshp  40162  lkrshp3  40163  lkrpssN  40220  cvrat2  40486  atcvrneN  40487  atcvrj2b  40489  2llnmat  40581  2lnat  40841  pmapjat1  40910  pclfinclN  41007  lautlt  41148  ltrn11at  41204  ltrnatneq  41239  trlcone  41785  tendoconid  41886  tendotr  41887  cdleml3N  42035  dochsordN  42431  dochn0nv  42432  djhcvat42  42472  dochsatshp  42508  lcfl8b  42561  lclkrlem2a  42564  lcfrlem9  42607  mapdsord  42712  mapdncol  42727  mapdpglem29  42757  mapdindp1  42777  hdmapnzcl  42902  hdmaprnlem1N  42906  hdmaprnlem3N  42907  hdmaprnlem3uN  42908  hdmaprnlem9N  42914  hdmap14lem9  42933  hgmapval1  42950  hgmapadd  42951  hgmapmul  42952  hgmaprnlem1N  42953  hdmaplkr  42970  hdmapip1  42973  hgmapvvlem1  42980  hgmapvvlem2  42981  hgmapvvlem3  42982  fldhmf1  43140  aks6d1c2p2  43169  aks6d1c5lem2  43188  aks6d1c6lem3  43222  redivne0bd  43501  fsuppind  43618  frlmnzcoordsca  43658  jm2.19  43999  jm2.26lem3  44007  kelac1  44064  mpaaeu  44151  radcnvrat  45297  binomcxplemnotnn0  45339  sqrtnegnre  48376  paireqne  48592  fmtnoprmfac1lem  48648  requad01  48718  requad2  48720  perfectALTVlem2  48819  nnsgrpnmnd  49274  isidom3  49441  rrx2pnedifcoorneor  49827  rrx2pnedifcoorneorr  49828  eenglngeehlnmlem2  49849  fdomne0  49959  oppcendc  50125  onetansqsecsq  50853