Theorem necon3bid 2972

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

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

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 2929

This theorem is referenced by:  neeq1d  2987  neeq2d  2988  neeq12d  2989  nebi  3008  pr1nebg  4807  f1dom3fv3dif  7202  frxp  8056  frxp2  8074  frxp3  8081  suppval1  8096  iinon  8260  fodomfib  9213  fodomfibOLD  9215  wemapso  9437  wemapso2lem  9438  infpssrlem4  10197  ttukeylem6  10405  fodomb  10417  tskcard  10672  addneintrd  11320  addneintr2d  11321  negne0bd  11465  negned  11469  subne0d  11481  subne0ad  11483  subneintrd  11516  subneintr2d  11518  divne0b  11787  div2neg  11844  divne1d  11908  div2sub  11946  xaddass2  13149  xadddi2  13196  seqf1olem1  13948  expne0  14000  sqne0  14030  hashneq0  14271  hashnncl  14273  hashgt0  14295  ccat1st1st  14536  pfxn0  14594  cjne0  15070  recval  15230  absgt0  15232  abs1m  15243  abslem2  15247  sqreulem  15267  sqreu  15268  absne0d  15357  geoserg  15773  geolim  15777  geolim2  15778  georeclim  15779  geoisum1c  15787  tanval2  16042  tanaddlem  16075  tanadd  16076  4sqlem11  16867  ipodrsima  18447  chnind  18527  chnub  18528  f1omvdmvd  19355  f1omvdcnv  19356  f1omvdconj  19358  pmtrfmvdn0  19374  sylow1lem4  19513  dprdf1o  19946  dprd2da  19956  ogrpsublt  20054  ringinvnz1ne0  20218  rrgsupp  20616  abvne0  20734  gzrngunit  21370  chrnzr  21467  obsne0  21662  mdetdiaglem  22513  cnhaus  23269  hauscmplem  23321  fsubbas  23782  metn0  24275  nmne0  24534  nmgt0  24545  iccpnfhmeo  24870  ncvs1  25084  ipcau2  25161  dvcnvlem  25907  dvlip  25925  ftc1lem5  25974  mdegldg  25998  ply1divmo  26068  ig1peu  26107  ig1pdvds  26112  dgrmul  26203  coecj  26211  coecjOLD  26213  plydivlem4  26231  vieta1lem2  26246  vieta1  26247  aareccl  26261  geolim3  26274  abelthlem2  26369  abelthlem7  26375  tanregt0  26475  tanarg  26555  logtayl  26596  abscxp2  26629  cxpsqrt  26639  abscxpbnd  26690  logrec  26700  ang180lem1  26746  ang180lem2  26747  ang180lem3  26748  lawcos  26753  isosctr  26758  asinlem  26805  atandm2  26814  atandm4  26816  2efiatan  26855  tanatan  26856  atandmtan  26857  dvatan  26872  mersenne  27165  perfectlem2  27168  dchrinv  27199  dchrptlem2  27203  dchrsum2  27206  sumdchr2  27208  lgsabs1  27274  dchrisum0re  27451  sltval2  27595  bday1s  27775  cuteq1  27778  n0subs2  28290  tgcgrneq  28461  footexALT  28696  footexlem1  28697  footexlem2  28698  colinearalg  28888  axsegconlem6  28900  axsegconlem9  28903  ax5seglem5  28911  axlowdimlem14  28933  wlkn0  29599  cyclnspth  29779  iswwlksnx  29818  wwlksm1edg  29859  wspthsnonn0vne  29895  umgrclwwlkge2  29971  clwwisshclwws  29995  hashecclwwlkn1  30057  umgrhashecclwwlk  30058  frgrregord013  30375  frgrogt3nreg  30377  friendshipgt3  30378  nrt2irr  30453  nvgt0  30654  nv1  30655  nmlnogt0  30777  nmblolbii  30779  blocnilem  30784  normne0  31110  normcan  31556  nmlnopne0  31979  nmophmi  32011  riesz3i  32042  hashne0  32792  wrdpmtrlast  33062  cycpmco2lem6  33100  1arithidom  33502  ply1unit  33538  m1pmeq  33547  minplyirredlem  33723  constrrtcclem  33747  constrconj  33758  iconstr  33779  zarclssn  33886  esumpcvgval  34091  ballotlemfrcn0  34543  signsply0  34564  signstfvn  34582  signsvtn0  34583  signstfvneq0  34585  signstfveq0a  34589  signshnz  34604  bnj168  34742  nummin  35104  usgrgt2cycl  35174  erdszelem9  35243  segcon2  36149  outsideofeu  36175  heicant  37705  smprngopr  38102  isfldidl2  38119  isdmn3  38124  lsat0cv  39142  lcvexchlem1  39143  lsatcvat2  39160  lkrshp  39214  lkrshp3  39215  lkrpssN  39272  cvrat2  39538  atcvrneN  39539  atcvrj2b  39541  2llnmat  39633  2lnat  39893  pmapjat1  39962  pclfinclN  40059  lautlt  40200  ltrn11at  40256  ltrnatneq  40291  trlcone  40837  tendoconid  40938  tendotr  40939  cdleml3N  41087  dochsordN  41483  dochn0nv  41484  djhcvat42  41524  dochsatshp  41560  lcfl8b  41613  lclkrlem2a  41616  lcfrlem9  41659  mapdsord  41764  mapdncol  41779  mapdpglem29  41809  mapdindp1  41829  hdmapnzcl  41954  hdmaprnlem1N  41958  hdmaprnlem3N  41959  hdmaprnlem3uN  41960  hdmaprnlem9N  41966  hdmap14lem9  41985  hgmapval1  42002  hgmapadd  42003  hgmapmul  42004  hgmaprnlem1N  42005  hdmaplkr  42022  hdmapip1  42025  hgmapvvlem1  42032  hgmapvvlem2  42033  hgmapvvlem3  42034  fldhmf1  42193  aks6d1c2p2  42222  aks6d1c5lem2  42241  aks6d1c6lem3  42275  fsuppind  42693  jm2.19  43096  jm2.26lem3  43104  kelac1  43166  mpaaeu  43253  radcnvrat  44417  binomcxplemnotnn0  44459  sqrtnegnre  47417  paireqne  47621  fmtnoprmfac1lem  47674  requad01  47731  requad2  47733  perfectALTVlem2  47832  nnsgrpnmnd  48288  rrx2pnedifcoorneor  48827  rrx2pnedifcoorneorr  48828  eenglngeehlnmlem2  48849  fdomne0  48960  oppcendc  49129  onetansqsecsq  49872