Theorem necon3bid 3060

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 3017	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3bid.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))
3	2	necon3bbid 3053	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ 𝐶 ≠ 𝐷))
4	1, 3	syl5bb 285	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   = wceq 1533   ≠ wne 3016

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 209  df-ne 3017

This theorem is referenced by:  neeq1d  3075  neeq2d  3076  neeq12d  3077  nebi  3096  pr1nebg  4781  f1dom3fv3dif  7020  frxp  7814  suppval1  7830  iinon  7971  fodomfib  8792  wemapso  9009  wemapso2lem  9010  infpssrlem4  9722  ttukeylem6  9930  fodomb  9942  tskcard  10197  addneintrd  10841  addneintr2d  10842  negne0bd  10984  negned  10988  subne0d  11000  subne0ad  11002  subneintrd  11035  subneintr2d  11037  divne0b  11303  div2neg  11357  divne1d  11421  div2sub  11459  xaddass2  12637  xadddi2  12684  seqf1olem1  13403  expne0  13454  sqne0  13483  hashneq0  13719  hashnncl  13721  hashgt0  13743  ccat1st1st  13978  pfxn0  14042  cjne0  14516  recval  14676  absgt0  14678  abs1m  14689  abslem2  14693  sqreulem  14713  sqreu  14714  absne0d  14801  geoserg  15215  geolim  15220  geolim2  15221  georeclim  15222  geoisum1c  15230  tanval2  15480  tanaddlem  15513  tanadd  15514  4sqlem11  16285  ipodrsima  17769  f1omvdmvd  18565  f1omvdcnv  18566  f1omvdconj  18568  pmtrfmvdn0  18584  sylow1lem4  18720  dprdf1o  19148  dprd2da  19158  ringinvnz1ne0  19336  abvne0  19592  rrgsupp  20058  mhpinvcl  20333  gzrngunit  20605  chrnzr  20671  obsne0  20863  mdetdiaglem  21201  cnhaus  21956  hauscmplem  22008  fsubbas  22469  metn0  22964  nmne0  23222  nmgt0  23233  iccpnfhmeo  23543  ncvs1  23755  ipcau2  23831  dvcnvlem  24567  dvlip  24584  ftc1lem5  24631  mdegldg  24654  ply1divmo  24723  ig1peu  24759  ig1pdvds  24764  dgrmul  24854  coecj  24862  plydivlem4  24879  vieta1lem2  24894  vieta1  24895  aareccl  24909  geolim3  24922  abelthlem2  25014  abelthlem7  25020  tanregt0  25117  tanarg  25196  logtayl  25237  abscxp2  25270  cxpsqrt  25280  abscxpbnd  25328  logrec  25335  ang180lem1  25381  ang180lem2  25382  ang180lem3  25383  lawcos  25388  isosctr  25393  asinlem  25440  atandm2  25449  atandm4  25451  2efiatan  25490  tanatan  25491  atandmtan  25492  dvatan  25507  mersenne  25797  perfectlem2  25800  dchrinv  25831  dchrptlem2  25835  dchrsum2  25838  sumdchr2  25840  lgsabs1  25906  dchrisum0re  26083  tgcgrneq  26263  footexALT  26498  footexlem1  26499  footexlem2  26500  colinearalg  26690  axsegconlem6  26702  axsegconlem9  26705  ax5seglem5  26713  axlowdimlem14  26735  wlkn0  27396  cyclnspth  27575  iswwlksnx  27612  wwlksm1edg  27653  wspthsnonn0vne  27690  umgrclwwlkge2  27763  clwwisshclwws  27787  hashecclwwlkn1  27850  umgrhashecclwwlk  27851  frgrregord013  28168  frgrogt3nreg  28170  friendshipgt3  28171  nvgt0  28445  nv1  28446  nmlnogt0  28568  nmblolbii  28570  blocnilem  28575  normne0  28901  normcan  29347  nmlnopne0  29770  nmophmi  29802  riesz3i  29833  ogrpsublt  30717  cycpmco2lem6  30768  esumpcvgval  31332  ballotlemfrcn0  31782  signsply0  31816  signstfvn  31834  signsvtn0  31835  signstfvneq0  31837  signstfveq0a  31841  signshnz  31856  bnj168  31995  usgrgt2cycl  32372  erdszelem9  32441  sltval2  33158  segcon2  33561  outsideofeu  33587  heicant  34921  smprngopr  35324  isfldidl2  35341  isdmn3  35346  lsat0cv  36163  lcvexchlem1  36164  lsatcvat2  36181  lkrshp  36235  lkrshp3  36236  lkrpssN  36293  cvrat2  36559  atcvrneN  36560  atcvrj2b  36562  2llnmat  36654  2lnat  36914  pmapjat1  36983  pclfinclN  37080  lautlt  37221  ltrn11at  37277  ltrnatneq  37312  trlcone  37858  tendoconid  37959  tendotr  37960  cdleml3N  38108  dochsordN  38504  dochn0nv  38505  djhcvat42  38545  dochsatshp  38581  lcfl8b  38634  lclkrlem2a  38637  lcfrlem9  38680  mapdsord  38785  mapdncol  38800  mapdpglem29  38830  mapdindp1  38850  hdmapnzcl  38975  hdmaprnlem1N  38979  hdmaprnlem3N  38980  hdmaprnlem3uN  38981  hdmaprnlem9N  38987  hdmap14lem9  39006  hgmapval1  39023  hgmapadd  39024  hgmapmul  39025  hgmaprnlem1N  39026  hdmaplkr  39043  hdmapip1  39046  hgmapvvlem1  39053  hgmapvvlem2  39054  hgmapvvlem3  39055  jm2.19  39583  jm2.26lem3  39591  kelac1  39656  mpaaeu  39743  radcnvrat  40639  binomcxplemnotnn0  40681  sqrtnegnre  43501  paireqne  43667  fmtnoprmfac1lem  43720  requad01  43780  requad2  43782  perfectALTVlem2  43881  nnsgrpnmnd  44079  rrx2pnedifcoorneor  44697  rrx2pnedifcoorneorr  44698  eenglngeehlnmlem2  44719  onetansqsecsq  44854