Theorem necon3bid 3031

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1538   ≠ wne 2987

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 210  df-ne 2988

This theorem is referenced by:  neeq1d  3046  neeq2d  3047  neeq12d  3048  nebi  3067  pr1nebg  4748  f1dom3fv3dif  7004  frxp  7803  suppval1  7819  iinon  7960  fodomfib  8782  wemapso  8999  wemapso2lem  9000  infpssrlem4  9717  ttukeylem6  9925  fodomb  9937  tskcard  10192  addneintrd  10836  addneintr2d  10837  negne0bd  10979  negned  10983  subne0d  10995  subne0ad  10997  subneintrd  11030  subneintr2d  11032  divne0b  11298  div2neg  11352  divne1d  11416  div2sub  11454  xaddass2  12631  xadddi2  12678  seqf1olem1  13405  expne0  13456  sqne0  13485  hashneq0  13721  hashnncl  13723  hashgt0  13745  ccat1st1st  13975  pfxn0  14039  cjne0  14514  recval  14674  absgt0  14676  abs1m  14687  abslem2  14691  sqreulem  14711  sqreu  14712  absne0d  14799  geoserg  15213  geolim  15218  geolim2  15219  georeclim  15220  geoisum1c  15228  tanval2  15478  tanaddlem  15511  tanadd  15512  4sqlem11  16281  ipodrsima  17767  f1omvdmvd  18563  f1omvdcnv  18564  f1omvdconj  18566  pmtrfmvdn0  18582  sylow1lem4  18718  dprdf1o  19147  dprd2da  19157  ringinvnz1ne0  19338  abvne0  19591  rrgsupp  20057  gzrngunit  20157  chrnzr  20222  obsne0  20414  mdetdiaglem  21203  cnhaus  21959  hauscmplem  22011  fsubbas  22472  metn0  22967  nmne0  23225  nmgt0  23236  iccpnfhmeo  23550  ncvs1  23762  ipcau2  23838  dvcnvlem  24579  dvlip  24596  ftc1lem5  24643  mdegldg  24667  ply1divmo  24736  ig1peu  24772  ig1pdvds  24777  dgrmul  24867  coecj  24875  plydivlem4  24892  vieta1lem2  24907  vieta1  24908  aareccl  24922  geolim3  24935  abelthlem2  25027  abelthlem7  25033  tanregt0  25131  tanarg  25210  logtayl  25251  abscxp2  25284  cxpsqrt  25294  abscxpbnd  25342  logrec  25349  ang180lem1  25395  ang180lem2  25396  ang180lem3  25397  lawcos  25402  isosctr  25407  asinlem  25454  atandm2  25463  atandm4  25465  2efiatan  25504  tanatan  25505  atandmtan  25506  dvatan  25521  mersenne  25811  perfectlem2  25814  dchrinv  25845  dchrptlem2  25849  dchrsum2  25852  sumdchr2  25854  lgsabs1  25920  dchrisum0re  26097  tgcgrneq  26277  footexALT  26512  footexlem1  26513  footexlem2  26514  colinearalg  26704  axsegconlem6  26716  axsegconlem9  26719  ax5seglem5  26727  axlowdimlem14  26749  wlkn0  27410  cyclnspth  27589  iswwlksnx  27626  wwlksm1edg  27667  wspthsnonn0vne  27703  umgrclwwlkge2  27776  clwwisshclwws  27800  hashecclwwlkn1  27862  umgrhashecclwwlk  27863  frgrregord013  28180  frgrogt3nreg  28182  friendshipgt3  28183  nvgt0  28457  nv1  28458  nmlnogt0  28580  nmblolbii  28582  blocnilem  28587  normne0  28913  normcan  29359  nmlnopne0  29782  nmophmi  29814  riesz3i  29845  ogrpsublt  30772  cycpmco2lem6  30823  zarclssn  31226  esumpcvgval  31447  ballotlemfrcn0  31897  signsply0  31931  signstfvn  31949  signsvtn0  31950  signstfvneq0  31952  signstfveq0a  31956  signshnz  31971  bnj168  32110  nummin  32474  usgrgt2cycl  32490  erdszelem9  32559  sltval2  33276  segcon2  33679  outsideofeu  33705  heicant  35092  smprngopr  35490  isfldidl2  35507  isdmn3  35512  lsat0cv  36329  lcvexchlem1  36330  lsatcvat2  36347  lkrshp  36401  lkrshp3  36402  lkrpssN  36459  cvrat2  36725  atcvrneN  36726  atcvrj2b  36728  2llnmat  36820  2lnat  37080  pmapjat1  37149  pclfinclN  37246  lautlt  37387  ltrn11at  37443  ltrnatneq  37478  trlcone  38024  tendoconid  38125  tendotr  38126  cdleml3N  38274  dochsordN  38670  dochn0nv  38671  djhcvat42  38711  dochsatshp  38747  lcfl8b  38800  lclkrlem2a  38803  lcfrlem9  38846  mapdsord  38951  mapdncol  38966  mapdpglem29  38996  mapdindp1  39016  hdmapnzcl  39141  hdmaprnlem1N  39145  hdmaprnlem3N  39146  hdmaprnlem3uN  39147  hdmaprnlem9N  39153  hdmap14lem9  39172  hgmapval1  39189  hgmapadd  39190  hgmapmul  39191  hgmaprnlem1N  39192  hdmaplkr  39209  hdmapip1  39212  hgmapvvlem1  39219  hgmapvvlem2  39220  hgmapvvlem3  39221  fsuppind  39456  jm2.19  39934  jm2.26lem3  39942  kelac1  40007  mpaaeu  40094  radcnvrat  41018  binomcxplemnotnn0  41060  sqrtnegnre  43864  paireqne  44028  fmtnoprmfac1lem  44081  requad01  44139  requad2  44141  perfectALTVlem2  44240  nnsgrpnmnd  44438  rrx2pnedifcoorneor  45130  rrx2pnedifcoorneorr  45131  eenglngeehlnmlem2  45152  onetansqsecsq  45287