Theorem necon3bid 2974

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

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

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 2931

This theorem is referenced by:  neeq1d  2989  neeq2d  2990  neeq12d  2991  nebi  3010  pr1nebg  4812  f1dom3fv3dif  7212  frxp  8066  frxp2  8084  frxp3  8091  suppval1  8106  iinon  8270  fodomfib  9227  fodomfibOLD  9229  wemapso  9454  wemapso2lem  9455  infpssrlem4  10214  ttukeylem6  10422  fodomb  10434  tskcard  10690  addneintrd  11338  addneintr2d  11339  negne0bd  11483  negned  11487  subne0d  11499  subne0ad  11501  subneintrd  11534  subneintr2d  11536  divne0b  11805  div2neg  11862  divne1d  11926  div2sub  11964  xaddass2  13163  xadddi2  13210  seqf1olem1  13962  expne0  14014  sqne0  14044  hashneq0  14285  hashnncl  14287  hashgt0  14309  ccat1st1st  14550  pfxn0  14608  cjne0  15084  recval  15244  absgt0  15246  abs1m  15257  abslem2  15261  sqreulem  15281  sqreu  15282  absne0d  15371  geoserg  15787  geolim  15791  geolim2  15792  georeclim  15793  geoisum1c  15801  tanval2  16056  tanaddlem  16089  tanadd  16090  4sqlem11  16881  ipodrsima  18462  chnind  18542  chnub  18543  f1omvdmvd  19370  f1omvdcnv  19371  f1omvdconj  19373  pmtrfmvdn0  19389  sylow1lem4  19528  dprdf1o  19961  dprd2da  19971  ogrpsublt  20069  ringinvnz1ne0  20233  rrgsupp  20632  abvne0  20750  gzrngunit  21386  chrnzr  21483  obsne0  21678  mdetdiaglem  22540  cnhaus  23296  hauscmplem  23348  fsubbas  23809  metn0  24302  nmne0  24561  nmgt0  24572  iccpnfhmeo  24897  ncvs1  25111  ipcau2  25188  dvcnvlem  25934  dvlip  25952  ftc1lem5  26001  mdegldg  26025  ply1divmo  26095  ig1peu  26134  ig1pdvds  26139  dgrmul  26230  coecj  26238  coecjOLD  26240  plydivlem4  26258  vieta1lem2  26273  vieta1  26274  aareccl  26288  geolim3  26301  abelthlem2  26396  abelthlem7  26402  tanregt0  26502  tanarg  26582  logtayl  26623  abscxp2  26656  cxpsqrt  26666  abscxpbnd  26717  logrec  26727  ang180lem1  26773  ang180lem2  26774  ang180lem3  26775  lawcos  26780  isosctr  26785  asinlem  26832  atandm2  26841  atandm4  26843  2efiatan  26882  tanatan  26883  atandmtan  26884  dvatan  26899  mersenne  27192  perfectlem2  27195  dchrinv  27226  dchrptlem2  27230  dchrsum2  27233  sumdchr2  27235  lgsabs1  27301  dchrisum0re  27478  sltval2  27622  bday1s  27802  cuteq1  27805  n0subs2  28323  tgcgrneq  28504  footexALT  28739  footexlem1  28740  footexlem2  28741  colinearalg  28932  axsegconlem6  28944  axsegconlem9  28947  ax5seglem5  28955  axlowdimlem14  28977  wlkn0  29643  cyclnspth  29823  iswwlksnx  29862  wwlksm1edg  29903  wspthsnonn0vne  29939  umgrclwwlkge2  30015  clwwisshclwws  30039  hashecclwwlkn1  30101  umgrhashecclwwlk  30102  frgrregord013  30419  frgrogt3nreg  30421  friendshipgt3  30422  nrt2irr  30497  nvgt0  30698  nv1  30699  nmlnogt0  30821  nmblolbii  30823  blocnilem  30828  normne0  31154  normcan  31600  nmlnopne0  32023  nmophmi  32055  riesz3i  32086  hashne0  32839  wrdpmtrlast  33124  cycpmco2lem6  33162  1arithidom  33567  ply1unit  33605  m1pmeq  33615  minplyirredlem  33816  constrrtcclem  33840  constrconj  33851  iconstr  33872  zarclssn  33979  esumpcvgval  34184  ballotlemfrcn0  34636  signsply0  34657  signstfvn  34675  signsvtn0  34676  signstfvneq0  34678  signstfveq0a  34682  signshnz  34697  bnj168  34835  nummin  35198  usgrgt2cycl  35273  erdszelem9  35342  segcon2  36248  outsideofeu  36274  heicant  37795  smprngopr  38192  isfldidl2  38209  isdmn3  38214  lsat0cv  39232  lcvexchlem1  39233  lsatcvat2  39250  lkrshp  39304  lkrshp3  39305  lkrpssN  39362  cvrat2  39628  atcvrneN  39629  atcvrj2b  39631  2llnmat  39723  2lnat  39983  pmapjat1  40052  pclfinclN  40149  lautlt  40290  ltrn11at  40346  ltrnatneq  40381  trlcone  40927  tendoconid  41028  tendotr  41029  cdleml3N  41177  dochsordN  41573  dochn0nv  41574  djhcvat42  41614  dochsatshp  41650  lcfl8b  41703  lclkrlem2a  41706  lcfrlem9  41749  mapdsord  41854  mapdncol  41869  mapdpglem29  41899  mapdindp1  41919  hdmapnzcl  42044  hdmaprnlem1N  42048  hdmaprnlem3N  42049  hdmaprnlem3uN  42050  hdmaprnlem9N  42056  hdmap14lem9  42075  hgmapval1  42092  hgmapadd  42093  hgmapmul  42094  hgmaprnlem1N  42095  hdmaplkr  42112  hdmapip1  42115  hgmapvvlem1  42122  hgmapvvlem2  42123  hgmapvvlem3  42124  fldhmf1  42283  aks6d1c2p2  42312  aks6d1c5lem2  42331  aks6d1c6lem3  42365  fsuppind  42775  jm2.19  43177  jm2.26lem3  43185  kelac1  43247  mpaaeu  43334  radcnvrat  44497  binomcxplemnotnn0  44539  sqrtnegnre  47495  paireqne  47699  fmtnoprmfac1lem  47752  requad01  47809  requad2  47811  perfectALTVlem2  47910  nnsgrpnmnd  48366  rrx2pnedifcoorneor  48904  rrx2pnedifcoorneorr  48905  eenglngeehlnmlem2  48926  fdomne0  49037  oppcendc  49205  onetansqsecsq  49948