Theorem necon3bid 2977

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

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

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 2934

This theorem is referenced by:  neeq1d  2992  neeq2d  2993  neeq12d  2994  nebi  3013  pr1nebg  4802  f1dom3fv3dif  7217  frxp  8070  frxp2  8088  frxp3  8095  suppval1  8110  iinon  8274  fodomfib  9233  fodomfibOLD  9235  wemapso  9460  wemapso2lem  9461  infpssrlem4  10222  ttukeylem6  10430  fodomb  10442  tskcard  10698  addneintrd  11347  addneintr2d  11348  negne0bd  11492  negned  11496  subne0d  11508  subne0ad  11510  subneintrd  11543  subneintr2d  11545  divne0b  11814  div2neg  11872  divne1d  11936  div2sub  11974  xaddass2  13196  xadddi2  13243  seqf1olem1  13997  expne0  14049  sqne0  14079  hashneq0  14320  hashnncl  14322  hashgt0  14344  ccat1st1st  14585  pfxn0  14643  cjne0  15119  recval  15279  absgt0  15281  abs1m  15292  abslem2  15296  sqreulem  15316  sqreu  15317  absne0d  15406  geoserg  15825  geolim  15829  geolim2  15830  georeclim  15831  geoisum1c  15839  tanval2  16094  tanaddlem  16127  tanadd  16128  4sqlem11  16920  ipodrsima  18501  chnind  18581  chnub  18582  f1omvdmvd  19412  f1omvdcnv  19413  f1omvdconj  19415  pmtrfmvdn0  19431  sylow1lem4  19570  dprdf1o  20003  dprd2da  20013  ogrpsublt  20111  ringinvnz1ne0  20275  rrgsupp  20672  abvne0  20790  gzrngunit  21426  chrnzr  21523  obsne0  21718  mdetdiaglem  22576  cnhaus  23332  hauscmplem  23384  fsubbas  23845  metn0  24338  nmne0  24597  nmgt0  24608  iccpnfhmeo  24925  ncvs1  25137  ipcau2  25214  dvcnvlem  25956  dvlip  25973  ftc1lem5  26020  mdegldg  26044  ply1divmo  26114  ig1peu  26153  ig1pdvds  26158  dgrmul  26248  coecj  26256  coecjOLD  26258  plydivlem4  26276  vieta1lem2  26291  vieta1  26292  aareccl  26306  geolim3  26319  abelthlem2  26413  abelthlem7  26419  tanregt0  26519  tanarg  26599  logtayl  26640  abscxp2  26673  cxpsqrt  26683  abscxpbnd  26733  logrec  26743  ang180lem1  26789  ang180lem2  26790  ang180lem3  26791  lawcos  26796  isosctr  26801  asinlem  26848  atandm2  26857  atandm4  26859  2efiatan  26898  tanatan  26899  atandmtan  26900  dvatan  26915  mersenne  27207  perfectlem2  27210  dchrinv  27241  dchrptlem2  27245  dchrsum2  27248  sumdchr2  27250  lgsabs1  27316  dchrisum0re  27493  ltsval2  27637  bday1  27823  cuteq1  27826  n0subs2  28373  tgcgrneq  28568  footexALT  28803  footexlem1  28804  footexlem2  28805  colinearalg  28996  axsegconlem6  29008  axsegconlem9  29011  ax5seglem5  29019  axlowdimlem14  29041  wlkn0  29707  cyclnspth  29887  iswwlksnx  29926  wwlksm1edg  29967  wspthsnonn0vne  30003  umgrclwwlkge2  30079  clwwisshclwws  30103  hashecclwwlkn1  30165  umgrhashecclwwlk  30166  frgrregord013  30483  frgrogt3nreg  30485  friendshipgt3  30486  nrt2irr  30561  nvgt0  30763  nv1  30764  nmlnogt0  30886  nmblolbii  30888  blocnilem  30893  normne0  31219  normcan  31665  nmlnopne0  32088  nmophmi  32120  riesz3i  32151  hashne0  32901  wrdpmtrlast  33172  cycpmco2lem6  33210  1arithidom  33615  ply1unit  33653  m1pmeq  33663  minplyirredlem  33873  constrrtcclem  33897  constrconj  33908  iconstr  33929  zarclssn  34036  esumpcvgval  34241  ballotlemfrcn0  34693  signsply0  34714  signstfvn  34732  signsvtn0  34733  signstfvneq0  34735  signstfveq0a  34739  signshnz  34754  bnj168  34892  nummin  35255  usgrgt2cycl  35331  erdszelem9  35400  segcon2  36306  outsideofeu  36332  heicant  37993  smprngopr  38390  isfldidl2  38407  isdmn3  38412  lsat0cv  39496  lcvexchlem1  39497  lsatcvat2  39514  lkrshp  39568  lkrshp3  39569  lkrpssN  39626  cvrat2  39892  atcvrneN  39893  atcvrj2b  39895  2llnmat  39987  2lnat  40247  pmapjat1  40316  pclfinclN  40413  lautlt  40554  ltrn11at  40610  ltrnatneq  40645  trlcone  41191  tendoconid  41292  tendotr  41293  cdleml3N  41441  dochsordN  41837  dochn0nv  41838  djhcvat42  41878  dochsatshp  41914  lcfl8b  41967  lclkrlem2a  41970  lcfrlem9  42013  mapdsord  42118  mapdncol  42133  mapdpglem29  42163  mapdindp1  42183  hdmapnzcl  42308  hdmaprnlem1N  42312  hdmaprnlem3N  42313  hdmaprnlem3uN  42314  hdmaprnlem9N  42320  hdmap14lem9  42339  hgmapval1  42356  hgmapadd  42357  hgmapmul  42358  hgmaprnlem1N  42359  hdmaplkr  42376  hdmapip1  42379  hgmapvvlem1  42386  hgmapvvlem2  42387  hgmapvvlem3  42388  fldhmf1  42546  aks6d1c2p2  42575  aks6d1c5lem2  42594  aks6d1c6lem3  42628  redivne0bd  42899  fsuppind  43040  jm2.19  43442  jm2.26lem3  43450  kelac1  43512  mpaaeu  43599  radcnvrat  44762  binomcxplemnotnn0  44804  sqrtnegnre  47770  paireqne  47986  fmtnoprmfac1lem  48042  requad01  48112  requad2  48114  perfectALTVlem2  48213  nnsgrpnmnd  48669  rrx2pnedifcoorneor  49207  rrx2pnedifcoorneorr  49208  eenglngeehlnmlem2  49229  fdomne0  49340  oppcendc  49508  onetansqsecsq  50251