Theorem necon3bid 2976

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

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

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 2933

This theorem is referenced by:  neeq1d  2991  neeq2d  2992  neeq12d  2993  nebi  3012  pr1nebg  4801  f1dom3fv3dif  7223  frxp  8076  frxp2  8094  frxp3  8101  suppval1  8116  iinon  8280  fodomfib  9239  fodomfibOLD  9241  wemapso  9466  wemapso2lem  9467  infpssrlem4  10228  ttukeylem6  10436  fodomb  10448  tskcard  10704  addneintrd  11353  addneintr2d  11354  negne0bd  11498  negned  11502  subne0d  11514  subne0ad  11516  subneintrd  11549  subneintr2d  11551  divne0b  11820  div2neg  11878  divne1d  11942  div2sub  11980  xaddass2  13202  xadddi2  13249  seqf1olem1  14003  expne0  14055  sqne0  14085  hashneq0  14326  hashnncl  14328  hashgt0  14350  ccat1st1st  14591  pfxn0  14649  cjne0  15125  recval  15285  absgt0  15287  abs1m  15298  abslem2  15302  sqreulem  15322  sqreu  15323  absne0d  15412  geoserg  15831  geolim  15835  geolim2  15836  georeclim  15837  geoisum1c  15845  tanval2  16100  tanaddlem  16133  tanadd  16134  4sqlem11  16926  ipodrsima  18507  chnind  18587  chnub  18588  f1omvdmvd  19418  f1omvdcnv  19419  f1omvdconj  19421  pmtrfmvdn0  19437  sylow1lem4  19576  dprdf1o  20009  dprd2da  20019  ogrpsublt  20117  ringinvnz1ne0  20281  rrgsupp  20678  abvne0  20796  gzrngunit  21413  chrnzr  21510  obsne0  21705  mdetdiaglem  22563  cnhaus  23319  hauscmplem  23371  fsubbas  23832  metn0  24325  nmne0  24584  nmgt0  24595  iccpnfhmeo  24912  ncvs1  25124  ipcau2  25201  dvcnvlem  25943  dvlip  25960  ftc1lem5  26007  mdegldg  26031  ply1divmo  26101  ig1peu  26140  ig1pdvds  26145  dgrmul  26235  coecj  26243  coecjOLD  26245  plydivlem4  26262  vieta1lem2  26277  vieta1  26278  aareccl  26292  geolim3  26305  abelthlem2  26397  abelthlem7  26403  tanregt0  26503  tanarg  26583  logtayl  26624  abscxp2  26657  cxpsqrt  26667  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  27190  perfectlem2  27193  dchrinv  27224  dchrptlem2  27228  dchrsum2  27231  sumdchr2  27233  lgsabs1  27299  dchrisum0re  27476  ltsval2  27620  bday1  27806  cuteq1  27809  n0subs2  28356  tgcgrneq  28551  footexALT  28786  footexlem1  28787  footexlem2  28788  colinearalg  28979  axsegconlem6  28991  axsegconlem9  28994  ax5seglem5  29002  axlowdimlem14  29024  wlkn0  29689  cyclnspth  29869  iswwlksnx  29908  wwlksm1edg  29949  wspthsnonn0vne  29985  umgrclwwlkge2  30061  clwwisshclwws  30085  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  frgrregord013  30465  frgrogt3nreg  30467  friendshipgt3  30468  nrt2irr  30543  nvgt0  30745  nv1  30746  nmlnogt0  30868  nmblolbii  30870  blocnilem  30875  normne0  31201  normcan  31647  nmlnopne0  32070  nmophmi  32102  riesz3i  32133  hashne0  32883  wrdpmtrlast  33154  cycpmco2lem6  33192  1arithidom  33597  ply1unit  33635  m1pmeq  33645  minplyirredlem  33854  constrrtcclem  33878  constrconj  33889  iconstr  33910  zarclssn  34017  esumpcvgval  34222  ballotlemfrcn0  34674  signsply0  34695  signstfvn  34713  signsvtn0  34714  signstfvneq0  34716  signstfveq0a  34720  signshnz  34735  bnj168  34873  nummin  35236  usgrgt2cycl  35312  erdszelem9  35381  segcon2  36287  outsideofeu  36313  heicant  37976  smprngopr  38373  isfldidl2  38390  isdmn3  38395  lsat0cv  39479  lcvexchlem1  39480  lsatcvat2  39497  lkrshp  39551  lkrshp3  39552  lkrpssN  39609  cvrat2  39875  atcvrneN  39876  atcvrj2b  39878  2llnmat  39970  2lnat  40230  pmapjat1  40299  pclfinclN  40396  lautlt  40537  ltrn11at  40593  ltrnatneq  40628  trlcone  41174  tendoconid  41275  tendotr  41276  cdleml3N  41424  dochsordN  41820  dochn0nv  41821  djhcvat42  41861  dochsatshp  41897  lcfl8b  41950  lclkrlem2a  41953  lcfrlem9  41996  mapdsord  42101  mapdncol  42116  mapdpglem29  42146  mapdindp1  42166  hdmapnzcl  42291  hdmaprnlem1N  42295  hdmaprnlem3N  42296  hdmaprnlem3uN  42297  hdmaprnlem9N  42303  hdmap14lem9  42322  hgmapval1  42339  hgmapadd  42340  hgmapmul  42341  hgmaprnlem1N  42342  hdmaplkr  42359  hdmapip1  42362  hgmapvvlem1  42369  hgmapvvlem2  42370  hgmapvvlem3  42371  fldhmf1  42529  aks6d1c2p2  42558  aks6d1c5lem2  42577  aks6d1c6lem3  42611  redivne0bd  42882  fsuppind  43023  jm2.19  43421  jm2.26lem3  43429  kelac1  43491  mpaaeu  43578  radcnvrat  44741  binomcxplemnotnn0  44783  sqrtnegnre  47755  paireqne  47971  fmtnoprmfac1lem  48027  requad01  48097  requad2  48099  perfectALTVlem2  48198  nnsgrpnmnd  48654  rrx2pnedifcoorneor  49192  rrx2pnedifcoorneorr  49193  eenglngeehlnmlem2  49214  fdomne0  49325  oppcendc  49493  onetansqsecsq  50236