Theorem necon3bid 2985

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

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

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 2941

This theorem is referenced by:  neeq1d  3000  neeq2d  3001  neeq12d  3002  nebi  3021  pr1nebg  4858  f1dom3fv3dif  7266  frxp  8111  frxp2  8129  frxp3  8136  suppval1  8151  iinon  8339  fodomfib  9325  wemapso  9545  wemapso2lem  9546  infpssrlem4  10300  ttukeylem6  10508  fodomb  10520  tskcard  10775  addneintrd  11420  addneintr2d  11421  negne0bd  11563  negned  11567  subne0d  11579  subne0ad  11581  subneintrd  11614  subneintr2d  11616  divne0b  11882  div2neg  11936  divne1d  12000  div2sub  12038  xaddass2  13228  xadddi2  13275  seqf1olem1  14006  expne0  14058  sqne0  14087  hashneq0  14323  hashnncl  14325  hashgt0  14347  ccat1st1st  14577  pfxn0  14635  cjne0  15109  recval  15268  absgt0  15270  abs1m  15281  abslem2  15285  sqreulem  15305  sqreu  15306  absne0d  15393  geoserg  15811  geolim  15815  geolim2  15816  georeclim  15817  geoisum1c  15825  tanval2  16075  tanaddlem  16108  tanadd  16109  4sqlem11  16887  ipodrsima  18493  f1omvdmvd  19310  f1omvdcnv  19311  f1omvdconj  19313  pmtrfmvdn0  19329  sylow1lem4  19468  dprdf1o  19901  dprd2da  19911  ringinvnz1ne0  20111  abvne0  20434  rrgsupp  20906  gzrngunit  21010  chrnzr  21081  obsne0  21279  mdetdiaglem  22099  cnhaus  22857  hauscmplem  22909  fsubbas  23370  metn0  23865  nmne0  24127  nmgt0  24138  iccpnfhmeo  24460  ncvs1  24673  ipcau2  24750  dvcnvlem  25492  dvlip  25509  ftc1lem5  25556  mdegldg  25583  ply1divmo  25652  ig1peu  25688  ig1pdvds  25693  dgrmul  25783  coecj  25791  plydivlem4  25808  vieta1lem2  25823  vieta1  25824  aareccl  25838  geolim3  25851  abelthlem2  25943  abelthlem7  25949  tanregt0  26047  tanarg  26126  logtayl  26167  abscxp2  26200  cxpsqrt  26210  abscxpbnd  26258  logrec  26265  ang180lem1  26311  ang180lem2  26312  ang180lem3  26313  lawcos  26318  isosctr  26323  asinlem  26370  atandm2  26379  atandm4  26381  2efiatan  26420  tanatan  26421  atandmtan  26422  dvatan  26437  mersenne  26727  perfectlem2  26730  dchrinv  26761  dchrptlem2  26765  dchrsum2  26768  sumdchr2  26770  lgsabs1  26836  dchrisum0re  27013  sltval2  27156  bday1s  27329  cuteq1  27331  tgcgrneq  27731  footexALT  27966  footexlem1  27967  footexlem2  27968  colinearalg  28165  axsegconlem6  28177  axsegconlem9  28180  ax5seglem5  28188  axlowdimlem14  28210  wlkn0  28875  cyclnspth  29054  iswwlksnx  29091  wwlksm1edg  29132  wspthsnonn0vne  29168  umgrclwwlkge2  29241  clwwisshclwws  29265  hashecclwwlkn1  29327  umgrhashecclwwlk  29328  frgrregord013  29645  frgrogt3nreg  29647  friendshipgt3  29648  nvgt0  29922  nv1  29923  nmlnogt0  30045  nmblolbii  30047  blocnilem  30052  normne0  30378  normcan  30824  nmlnopne0  31247  nmophmi  31279  riesz3i  31310  ogrpsublt  32234  cycpmco2lem6  32285  minplyirredlem  32764  zarclssn  32848  esumpcvgval  33071  ballotlemfrcn0  33523  signsply0  33557  signstfvn  33575  signsvtn0  33576  signstfvneq0  33578  signstfveq0a  33582  signshnz  33597  bnj168  33736  nummin  34089  usgrgt2cycl  34116  erdszelem9  34185  segcon2  35072  outsideofeu  35098  heicant  36518  smprngopr  36915  isfldidl2  36932  isdmn3  36937  lsat0cv  37898  lcvexchlem1  37899  lsatcvat2  37916  lkrshp  37970  lkrshp3  37971  lkrpssN  38028  cvrat2  38295  atcvrneN  38296  atcvrj2b  38298  2llnmat  38390  2lnat  38650  pmapjat1  38719  pclfinclN  38816  lautlt  38957  ltrn11at  39013  ltrnatneq  39048  trlcone  39594  tendoconid  39695  tendotr  39696  cdleml3N  39844  dochsordN  40240  dochn0nv  40241  djhcvat42  40281  dochsatshp  40317  lcfl8b  40370  lclkrlem2a  40373  lcfrlem9  40416  mapdsord  40521  mapdncol  40536  mapdpglem29  40566  mapdindp1  40586  hdmapnzcl  40711  hdmaprnlem1N  40715  hdmaprnlem3N  40716  hdmaprnlem3uN  40717  hdmaprnlem9N  40723  hdmap14lem9  40742  hgmapval1  40759  hgmapadd  40760  hgmapmul  40761  hgmaprnlem1N  40762  hdmaplkr  40779  hdmapip1  40782  hgmapvvlem1  40789  hgmapvvlem2  40790  hgmapvvlem3  40791  fldhmf1  40950  aks6d1c2p2  40952  fsuppind  41164  jm2.19  41722  jm2.26lem3  41730  kelac1  41795  mpaaeu  41882  radcnvrat  43063  binomcxplemnotnn0  43105  sqrtnegnre  46005  paireqne  46169  fmtnoprmfac1lem  46222  requad01  46279  requad2  46281  perfectALTVlem2  46380  nnsgrpnmnd  46578  rrx2pnedifcoorneor  47392  rrx2pnedifcoorneorr  47393  eenglngeehlnmlem2  47414  fdomne0  47506  onetansqsecsq  47796