Theorem necon3bid 2975

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

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

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 2932

This theorem is referenced by:  neeq1d  2990  neeq2d  2991  neeq12d  2992  nebi  3011  pr1nebg  4838  f1dom3fv3dif  7270  frxp  8133  frxp2  8151  frxp3  8158  suppval1  8173  iinon  8362  fodomfib  9351  fodomfibOLD  9353  wemapso  9573  wemapso2lem  9574  infpssrlem4  10328  ttukeylem6  10536  fodomb  10548  tskcard  10803  addneintrd  11450  addneintr2d  11451  negne0bd  11595  negned  11599  subne0d  11611  subne0ad  11613  subneintrd  11646  subneintr2d  11648  divne0b  11915  div2neg  11972  divne1d  12036  div2sub  12074  xaddass2  13274  xadddi2  13321  seqf1olem1  14064  expne0  14116  sqne0  14145  hashneq0  14385  hashnncl  14387  hashgt0  14409  ccat1st1st  14648  pfxn0  14706  cjne0  15184  recval  15343  absgt0  15345  abs1m  15356  abslem2  15360  sqreulem  15380  sqreu  15381  absne0d  15468  geoserg  15884  geolim  15888  geolim2  15889  georeclim  15890  geoisum1c  15898  tanval2  16151  tanaddlem  16184  tanadd  16185  4sqlem11  16975  ipodrsima  18555  f1omvdmvd  19429  f1omvdcnv  19430  f1omvdconj  19432  pmtrfmvdn0  19448  sylow1lem4  19587  dprdf1o  20020  dprd2da  20030  ringinvnz1ne0  20265  rrgsupp  20669  abvne0  20788  gzrngunit  21413  chrnzr  21503  obsne0  21699  mdetdiaglem  22552  cnhaus  23308  hauscmplem  23360  fsubbas  23821  metn0  24315  nmne0  24576  nmgt0  24587  iccpnfhmeo  24912  ncvs1  25127  ipcau2  25204  dvcnvlem  25950  dvlip  25968  ftc1lem5  26017  mdegldg  26041  ply1divmo  26111  ig1peu  26150  ig1pdvds  26155  dgrmul  26246  coecj  26254  coecjOLD  26256  plydivlem4  26274  vieta1lem2  26289  vieta1  26290  aareccl  26304  geolim3  26317  abelthlem2  26412  abelthlem7  26418  tanregt0  26517  tanarg  26597  logtayl  26638  abscxp2  26671  cxpsqrt  26681  abscxpbnd  26732  logrec  26742  ang180lem1  26788  ang180lem2  26789  ang180lem3  26790  lawcos  26795  isosctr  26800  asinlem  26847  atandm2  26856  atandm4  26858  2efiatan  26897  tanatan  26898  atandmtan  26899  dvatan  26914  mersenne  27207  perfectlem2  27210  dchrinv  27241  dchrptlem2  27245  dchrsum2  27248  sumdchr2  27250  lgsabs1  27316  dchrisum0re  27493  sltval2  27637  bday1s  27812  cuteq1  27814  tgcgrneq  28427  footexALT  28662  footexlem1  28663  footexlem2  28664  colinearalg  28855  axsegconlem6  28867  axsegconlem9  28870  ax5seglem5  28878  axlowdimlem14  28900  wlkn0  29567  cyclnspth  29749  iswwlksnx  29788  wwlksm1edg  29829  wspthsnonn0vne  29865  umgrclwwlkge2  29938  clwwisshclwws  29962  hashecclwwlkn1  30024  umgrhashecclwwlk  30025  frgrregord013  30342  frgrogt3nreg  30344  friendshipgt3  30345  nrt2irr  30420  nvgt0  30621  nv1  30622  nmlnogt0  30744  nmblolbii  30746  blocnilem  30751  normne0  31077  normcan  31523  nmlnopne0  31946  nmophmi  31978  riesz3i  32009  hashne0  32753  chnind  32940  chnub  32941  ogrpsublt  33037  wrdpmtrlast  33052  cycpmco2lem6  33090  1arithidom  33500  ply1unit  33535  m1pmeq  33543  minplyirredlem  33690  constrrtcclem  33714  constrconj  33725  iconstr  33746  zarclssn  33831  esumpcvgval  34038  ballotlemfrcn0  34491  signsply0  34525  signstfvn  34543  signsvtn0  34544  signstfvneq0  34546  signstfveq0a  34550  signshnz  34565  bnj168  34703  nummin  35064  usgrgt2cycl  35094  erdszelem9  35163  segcon2  36065  outsideofeu  36091  heicant  37621  smprngopr  38018  isfldidl2  38035  isdmn3  38040  lsat0cv  38993  lcvexchlem1  38994  lsatcvat2  39011  lkrshp  39065  lkrshp3  39066  lkrpssN  39123  cvrat2  39390  atcvrneN  39391  atcvrj2b  39393  2llnmat  39485  2lnat  39745  pmapjat1  39814  pclfinclN  39911  lautlt  40052  ltrn11at  40108  ltrnatneq  40143  trlcone  40689  tendoconid  40790  tendotr  40791  cdleml3N  40939  dochsordN  41335  dochn0nv  41336  djhcvat42  41376  dochsatshp  41412  lcfl8b  41465  lclkrlem2a  41468  lcfrlem9  41511  mapdsord  41616  mapdncol  41631  mapdpglem29  41661  mapdindp1  41681  hdmapnzcl  41806  hdmaprnlem1N  41810  hdmaprnlem3N  41811  hdmaprnlem3uN  41812  hdmaprnlem9N  41818  hdmap14lem9  41837  hgmapval1  41854  hgmapadd  41855  hgmapmul  41856  hgmaprnlem1N  41857  hdmaplkr  41874  hdmapip1  41877  hgmapvvlem1  41884  hgmapvvlem2  41885  hgmapvvlem3  41886  fldhmf1  42050  aks6d1c2p2  42079  aks6d1c5lem2  42098  aks6d1c6lem3  42132  fsuppind  42563  jm2.19  42968  jm2.26lem3  42976  kelac1  43038  mpaaeu  43125  radcnvrat  44290  binomcxplemnotnn0  44332  sqrtnegnre  47277  paireqne  47456  fmtnoprmfac1lem  47509  requad01  47566  requad2  47568  perfectALTVlem2  47667  nnsgrpnmnd  48052  rrx2pnedifcoorneor  48595  rrx2pnedifcoorneorr  48596  eenglngeehlnmlem2  48617  fdomne0  48717  oppcendc  48874  onetansqsecsq  49288