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

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

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 2930

This theorem is referenced by:  neeq1d  2989  neeq2d  2990  neeq12d  2991  nebi  3010  pr1nebg  4860  f1dom3fv3dif  7278  frxp  8131  frxp2  8149  frxp3  8156  suppval1  8171  iinon  8361  fodomfib  9352  wemapso  9576  wemapso2lem  9577  infpssrlem4  10331  ttukeylem6  10539  fodomb  10551  tskcard  10806  addneintrd  11453  addneintr2d  11454  negne0bd  11596  negned  11600  subne0d  11612  subne0ad  11614  subneintrd  11647  subneintr2d  11649  divne0b  11916  div2neg  11970  divne1d  12034  div2sub  12072  xaddass2  13264  xadddi2  13311  seqf1olem1  14042  expne0  14094  sqne0  14123  hashneq0  14359  hashnncl  14361  hashgt0  14383  ccat1st1st  14614  pfxn0  14672  cjne0  15146  recval  15305  absgt0  15307  abs1m  15318  abslem2  15322  sqreulem  15342  sqreu  15343  absne0d  15430  geoserg  15848  geolim  15852  geolim2  15853  georeclim  15854  geoisum1c  15862  tanval2  16113  tanaddlem  16146  tanadd  16147  4sqlem11  16927  ipodrsima  18536  f1omvdmvd  19410  f1omvdcnv  19411  f1omvdconj  19413  pmtrfmvdn0  19429  sylow1lem4  19568  dprdf1o  20001  dprd2da  20011  ringinvnz1ne0  20248  abvne0  20719  rrgsupp  21255  gzrngunit  21383  chrnzr  21477  obsne0  21676  mdetdiaglem  22544  cnhaus  23302  hauscmplem  23354  fsubbas  23815  metn0  24310  nmne0  24572  nmgt0  24583  iccpnfhmeo  24914  ncvs1  25129  ipcau2  25206  dvcnvlem  25952  dvlip  25970  ftc1lem5  26019  mdegldg  26046  ply1divmo  26116  ig1peu  26154  ig1pdvds  26159  dgrmul  26250  coecj  26258  plydivlem4  26276  vieta1lem2  26291  vieta1  26292  aareccl  26306  geolim3  26319  abelthlem2  26414  abelthlem7  26420  tanregt0  26518  tanarg  26598  logtayl  26639  abscxp2  26672  cxpsqrt  26682  abscxpbnd  26733  logrec  26740  ang180lem1  26786  ang180lem2  26787  ang180lem3  26788  lawcos  26793  isosctr  26798  asinlem  26845  atandm2  26854  atandm4  26856  2efiatan  26895  tanatan  26896  atandmtan  26897  dvatan  26912  mersenne  27205  perfectlem2  27208  dchrinv  27239  dchrptlem2  27243  dchrsum2  27246  sumdchr2  27248  lgsabs1  27314  dchrisum0re  27491  sltval2  27635  bday1s  27810  cuteq1  27812  tgcgrneq  28359  footexALT  28594  footexlem1  28595  footexlem2  28596  colinearalg  28793  axsegconlem6  28805  axsegconlem9  28808  ax5seglem5  28816  axlowdimlem14  28838  wlkn0  29507  cyclnspth  29686  iswwlksnx  29723  wwlksm1edg  29764  wspthsnonn0vne  29800  umgrclwwlkge2  29873  clwwisshclwws  29897  hashecclwwlkn1  29959  umgrhashecclwwlk  29960  frgrregord013  30277  frgrogt3nreg  30279  friendshipgt3  30280  nrt2irr  30355  nvgt0  30556  nv1  30557  nmlnogt0  30679  nmblolbii  30681  blocnilem  30686  normne0  31012  normcan  31458  nmlnopne0  31881  nmophmi  31913  riesz3i  31944  ogrpsublt  32891  wrdpmtrlast  32906  cycpmco2lem6  32944  1arithidom  33349  ply1unit  33386  m1pmeq  33392  minplyirredlem  33511  zarclssn  33605  esumpcvgval  33828  ballotlemfrcn0  34280  signsply0  34314  signstfvn  34332  signsvtn0  34333  signstfvneq0  34335  signstfveq0a  34339  signshnz  34354  bnj168  34492  nummin  34845  usgrgt2cycl  34871  erdszelem9  34940  segcon2  35832  outsideofeu  35858  heicant  37259  smprngopr  37656  isfldidl2  37673  isdmn3  37678  lsat0cv  38635  lcvexchlem1  38636  lsatcvat2  38653  lkrshp  38707  lkrshp3  38708  lkrpssN  38765  cvrat2  39032  atcvrneN  39033  atcvrj2b  39035  2llnmat  39127  2lnat  39387  pmapjat1  39456  pclfinclN  39553  lautlt  39694  ltrn11at  39750  ltrnatneq  39785  trlcone  40331  tendoconid  40432  tendotr  40433  cdleml3N  40581  dochsordN  40977  dochn0nv  40978  djhcvat42  41018  dochsatshp  41054  lcfl8b  41107  lclkrlem2a  41110  lcfrlem9  41153  mapdsord  41258  mapdncol  41273  mapdpglem29  41303  mapdindp1  41323  hdmapnzcl  41448  hdmaprnlem1N  41452  hdmaprnlem3N  41453  hdmaprnlem3uN  41454  hdmaprnlem9N  41460  hdmap14lem9  41479  hgmapval1  41496  hgmapadd  41497  hgmapmul  41498  hgmaprnlem1N  41499  hdmaplkr  41516  hdmapip1  41519  hgmapvvlem1  41526  hgmapvvlem2  41527  hgmapvvlem3  41528  fldhmf1  41693  aks6d1c2p2  41722  aks6d1c5lem2  41741  aks6d1c6lem3  41775  fsuppind  41958  jm2.19  42556  jm2.26lem3  42564  kelac1  42629  mpaaeu  42716  radcnvrat  43893  binomcxplemnotnn0  43935  sqrtnegnre  46825  paireqne  46988  fmtnoprmfac1lem  47041  requad01  47098  requad2  47100  perfectALTVlem2  47199  nnsgrpnmnd  47426  rrx2pnedifcoorneor  47975  rrx2pnedifcoorneorr  47976  eenglngeehlnmlem2  47997  fdomne0  48088  onetansqsecsq  48378