Theorem necon3bid 2970

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

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

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 2927

This theorem is referenced by:  neeq1d  2985  neeq2d  2986  neeq12d  2987  nebi  3006  pr1nebg  4825  f1dom3fv3dif  7246  frxp  8108  frxp2  8126  frxp3  8133  suppval1  8148  iinon  8312  fodomfib  9287  fodomfibOLD  9289  wemapso  9511  wemapso2lem  9512  infpssrlem4  10266  ttukeylem6  10474  fodomb  10486  tskcard  10741  addneintrd  11388  addneintr2d  11389  negne0bd  11533  negned  11537  subne0d  11549  subne0ad  11551  subneintrd  11584  subneintr2d  11586  divne0b  11855  div2neg  11912  divne1d  11976  div2sub  12014  xaddass2  13217  xadddi2  13264  seqf1olem1  14013  expne0  14065  sqne0  14095  hashneq0  14336  hashnncl  14338  hashgt0  14360  ccat1st1st  14600  pfxn0  14658  cjne0  15136  recval  15296  absgt0  15298  abs1m  15309  abslem2  15313  sqreulem  15333  sqreu  15334  absne0d  15423  geoserg  15839  geolim  15843  geolim2  15844  georeclim  15845  geoisum1c  15853  tanval2  16108  tanaddlem  16141  tanadd  16142  4sqlem11  16933  ipodrsima  18507  f1omvdmvd  19380  f1omvdcnv  19381  f1omvdconj  19383  pmtrfmvdn0  19399  sylow1lem4  19538  dprdf1o  19971  dprd2da  19981  ringinvnz1ne0  20216  rrgsupp  20617  abvne0  20735  gzrngunit  21357  chrnzr  21447  obsne0  21641  mdetdiaglem  22492  cnhaus  23248  hauscmplem  23300  fsubbas  23761  metn0  24255  nmne0  24514  nmgt0  24525  iccpnfhmeo  24850  ncvs1  25064  ipcau2  25141  dvcnvlem  25887  dvlip  25905  ftc1lem5  25954  mdegldg  25978  ply1divmo  26048  ig1peu  26087  ig1pdvds  26092  dgrmul  26183  coecj  26191  coecjOLD  26193  plydivlem4  26211  vieta1lem2  26226  vieta1  26227  aareccl  26241  geolim3  26254  abelthlem2  26349  abelthlem7  26355  tanregt0  26455  tanarg  26535  logtayl  26576  abscxp2  26609  cxpsqrt  26619  abscxpbnd  26670  logrec  26680  ang180lem1  26726  ang180lem2  26727  ang180lem3  26728  lawcos  26733  isosctr  26738  asinlem  26785  atandm2  26794  atandm4  26796  2efiatan  26835  tanatan  26836  atandmtan  26837  dvatan  26852  mersenne  27145  perfectlem2  27148  dchrinv  27179  dchrptlem2  27183  dchrsum2  27186  sumdchr2  27188  lgsabs1  27254  dchrisum0re  27431  sltval2  27575  bday1s  27750  cuteq1  27753  n0subs2  28261  tgcgrneq  28417  footexALT  28652  footexlem1  28653  footexlem2  28654  colinearalg  28844  axsegconlem6  28856  axsegconlem9  28859  ax5seglem5  28867  axlowdimlem14  28889  wlkn0  29556  cyclnspth  29738  iswwlksnx  29777  wwlksm1edg  29818  wspthsnonn0vne  29854  umgrclwwlkge2  29927  clwwisshclwws  29951  hashecclwwlkn1  30013  umgrhashecclwwlk  30014  frgrregord013  30331  frgrogt3nreg  30333  friendshipgt3  30334  nrt2irr  30409  nvgt0  30610  nv1  30611  nmlnogt0  30733  nmblolbii  30735  blocnilem  30740  normne0  31066  normcan  31512  nmlnopne0  31935  nmophmi  31967  riesz3i  31998  hashne0  32742  chnind  32944  chnub  32945  ogrpsublt  33042  wrdpmtrlast  33057  cycpmco2lem6  33095  1arithidom  33515  ply1unit  33551  m1pmeq  33559  minplyirredlem  33707  constrrtcclem  33731  constrconj  33742  iconstr  33763  zarclssn  33870  esumpcvgval  34075  ballotlemfrcn0  34528  signsply0  34549  signstfvn  34567  signsvtn0  34568  signstfvneq0  34570  signstfveq0a  34574  signshnz  34589  bnj168  34727  nummin  35088  usgrgt2cycl  35124  erdszelem9  35193  segcon2  36100  outsideofeu  36126  heicant  37656  smprngopr  38053  isfldidl2  38070  isdmn3  38075  lsat0cv  39033  lcvexchlem1  39034  lsatcvat2  39051  lkrshp  39105  lkrshp3  39106  lkrpssN  39163  cvrat2  39430  atcvrneN  39431  atcvrj2b  39433  2llnmat  39525  2lnat  39785  pmapjat1  39854  pclfinclN  39951  lautlt  40092  ltrn11at  40148  ltrnatneq  40183  trlcone  40729  tendoconid  40830  tendotr  40831  cdleml3N  40979  dochsordN  41375  dochn0nv  41376  djhcvat42  41416  dochsatshp  41452  lcfl8b  41505  lclkrlem2a  41508  lcfrlem9  41551  mapdsord  41656  mapdncol  41671  mapdpglem29  41701  mapdindp1  41721  hdmapnzcl  41846  hdmaprnlem1N  41850  hdmaprnlem3N  41851  hdmaprnlem3uN  41852  hdmaprnlem9N  41858  hdmap14lem9  41877  hgmapval1  41894  hgmapadd  41895  hgmapmul  41896  hgmaprnlem1N  41897  hdmaplkr  41914  hdmapip1  41917  hgmapvvlem1  41924  hgmapvvlem2  41925  hgmapvvlem3  41926  fldhmf1  42085  aks6d1c2p2  42114  aks6d1c5lem2  42133  aks6d1c6lem3  42167  fsuppind  42585  jm2.19  42989  jm2.26lem3  42997  kelac1  43059  mpaaeu  43146  radcnvrat  44310  binomcxplemnotnn0  44352  sqrtnegnre  47312  paireqne  47516  fmtnoprmfac1lem  47569  requad01  47626  requad2  47628  perfectALTVlem2  47727  nnsgrpnmnd  48170  rrx2pnedifcoorneor  48709  rrx2pnedifcoorneorr  48710  eenglngeehlnmlem2  48731  fdomne0  48842  oppcendc  49011  onetansqsecsq  49754