Theorem necon3bid 2982

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   = wceq 1536   ≠ wne 2937

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 207  df-ne 2938

This theorem is referenced by:  neeq1d  2997  neeq2d  2998  neeq12d  2999  nebi  3018  pr1nebg  4862  f1dom3fv3dif  7287  frxp  8149  frxp2  8167  frxp3  8174  suppval1  8189  iinon  8378  fodomfib  9366  fodomfibOLD  9368  wemapso  9588  wemapso2lem  9589  infpssrlem4  10343  ttukeylem6  10551  fodomb  10563  tskcard  10818  addneintrd  11465  addneintr2d  11466  negne0bd  11610  negned  11614  subne0d  11626  subne0ad  11628  subneintrd  11661  subneintr2d  11663  divne0b  11930  div2neg  11987  divne1d  12051  div2sub  12089  xaddass2  13288  xadddi2  13335  seqf1olem1  14078  expne0  14130  sqne0  14159  hashneq0  14399  hashnncl  14401  hashgt0  14423  ccat1st1st  14662  pfxn0  14720  cjne0  15198  recval  15357  absgt0  15359  abs1m  15370  abslem2  15374  sqreulem  15394  sqreu  15395  absne0d  15482  geoserg  15898  geolim  15902  geolim2  15903  georeclim  15904  geoisum1c  15912  tanval2  16165  tanaddlem  16198  tanadd  16199  4sqlem11  16988  ipodrsima  18598  f1omvdmvd  19475  f1omvdcnv  19476  f1omvdconj  19478  pmtrfmvdn0  19494  sylow1lem4  19633  dprdf1o  20066  dprd2da  20076  ringinvnz1ne0  20313  rrgsupp  20717  abvne0  20836  gzrngunit  21468  chrnzr  21562  obsne0  21762  mdetdiaglem  22619  cnhaus  23377  hauscmplem  23429  fsubbas  23890  metn0  24385  nmne0  24647  nmgt0  24658  iccpnfhmeo  24989  ncvs1  25204  ipcau2  25281  dvcnvlem  26028  dvlip  26046  ftc1lem5  26095  mdegldg  26119  ply1divmo  26189  ig1peu  26228  ig1pdvds  26233  dgrmul  26324  coecj  26332  coecjOLD  26334  plydivlem4  26352  vieta1lem2  26367  vieta1  26368  aareccl  26382  geolim3  26395  abelthlem2  26490  abelthlem7  26496  tanregt0  26595  tanarg  26675  logtayl  26716  abscxp2  26749  cxpsqrt  26759  abscxpbnd  26810  logrec  26820  ang180lem1  26866  ang180lem2  26867  ang180lem3  26868  lawcos  26873  isosctr  26878  asinlem  26925  atandm2  26934  atandm4  26936  2efiatan  26975  tanatan  26976  atandmtan  26977  dvatan  26992  mersenne  27285  perfectlem2  27288  dchrinv  27319  dchrptlem2  27323  dchrsum2  27326  sumdchr2  27328  lgsabs1  27394  dchrisum0re  27571  sltval2  27715  bday1s  27890  cuteq1  27892  tgcgrneq  28505  footexALT  28740  footexlem1  28741  footexlem2  28742  colinearalg  28939  axsegconlem6  28951  axsegconlem9  28954  ax5seglem5  28962  axlowdimlem14  28984  wlkn0  29653  cyclnspth  29832  iswwlksnx  29869  wwlksm1edg  29910  wspthsnonn0vne  29946  umgrclwwlkge2  30019  clwwisshclwws  30043  hashecclwwlkn1  30105  umgrhashecclwwlk  30106  frgrregord013  30423  frgrogt3nreg  30425  friendshipgt3  30426  nrt2irr  30501  nvgt0  30702  nv1  30703  nmlnogt0  30825  nmblolbii  30827  blocnilem  30832  normne0  31158  normcan  31604  nmlnopne0  32027  nmophmi  32059  riesz3i  32090  chnind  32984  chnub  32985  ogrpsublt  33080  wrdpmtrlast  33095  cycpmco2lem6  33133  1arithidom  33544  ply1unit  33579  m1pmeq  33587  minplyirredlem  33717  constrrtcclem  33739  constrconj  33749  zarclssn  33833  esumpcvgval  34058  ballotlemfrcn0  34510  signsply0  34544  signstfvn  34562  signsvtn0  34563  signstfvneq0  34565  signstfveq0a  34569  signshnz  34584  bnj168  34722  nummin  35083  usgrgt2cycl  35114  erdszelem9  35183  segcon2  36086  outsideofeu  36112  heicant  37641  smprngopr  38038  isfldidl2  38055  isdmn3  38060  lsat0cv  39014  lcvexchlem1  39015  lsatcvat2  39032  lkrshp  39086  lkrshp3  39087  lkrpssN  39144  cvrat2  39411  atcvrneN  39412  atcvrj2b  39414  2llnmat  39506  2lnat  39766  pmapjat1  39835  pclfinclN  39932  lautlt  40073  ltrn11at  40129  ltrnatneq  40164  trlcone  40710  tendoconid  40811  tendotr  40812  cdleml3N  40960  dochsordN  41356  dochn0nv  41357  djhcvat42  41397  dochsatshp  41433  lcfl8b  41486  lclkrlem2a  41489  lcfrlem9  41532  mapdsord  41637  mapdncol  41652  mapdpglem29  41682  mapdindp1  41702  hdmapnzcl  41827  hdmaprnlem1N  41831  hdmaprnlem3N  41832  hdmaprnlem3uN  41833  hdmaprnlem9N  41839  hdmap14lem9  41858  hgmapval1  41875  hgmapadd  41876  hgmapmul  41877  hgmaprnlem1N  41878  hdmaplkr  41895  hdmapip1  41898  hgmapvvlem1  41905  hgmapvvlem2  41906  hgmapvvlem3  41907  fldhmf1  42071  aks6d1c2p2  42100  aks6d1c5lem2  42119  aks6d1c6lem3  42153  fsuppind  42576  jm2.19  42981  jm2.26lem3  42989  kelac1  43051  mpaaeu  43138  radcnvrat  44309  binomcxplemnotnn0  44351  sqrtnegnre  47256  paireqne  47435  fmtnoprmfac1lem  47488  requad01  47545  requad2  47547  perfectALTVlem2  47646  nnsgrpnmnd  48021  rrx2pnedifcoorneor  48565  rrx2pnedifcoorneorr  48566  eenglngeehlnmlem2  48587  fdomne0  48679  onetansqsecsq  48991