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 1541   ≠ 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  4814  f1dom3fv3dif  7214  frxp  8068  frxp2  8086  frxp3  8093  suppval1  8108  iinon  8272  fodomfib  9229  fodomfibOLD  9231  wemapso  9456  wemapso2lem  9457  infpssrlem4  10216  ttukeylem6  10424  fodomb  10436  tskcard  10692  addneintrd  11340  addneintr2d  11341  negne0bd  11485  negned  11489  subne0d  11501  subne0ad  11503  subneintrd  11536  subneintr2d  11538  divne0b  11807  div2neg  11864  divne1d  11928  div2sub  11966  xaddass2  13165  xadddi2  13212  seqf1olem1  13964  expne0  14016  sqne0  14046  hashneq0  14287  hashnncl  14289  hashgt0  14311  ccat1st1st  14552  pfxn0  14610  cjne0  15086  recval  15246  absgt0  15248  abs1m  15259  abslem2  15263  sqreulem  15283  sqreu  15284  absne0d  15373  geoserg  15789  geolim  15793  geolim2  15794  georeclim  15795  geoisum1c  15803  tanval2  16058  tanaddlem  16091  tanadd  16092  4sqlem11  16883  ipodrsima  18464  chnind  18544  chnub  18545  f1omvdmvd  19372  f1omvdcnv  19373  f1omvdconj  19375  pmtrfmvdn0  19391  sylow1lem4  19530  dprdf1o  19963  dprd2da  19973  ogrpsublt  20071  ringinvnz1ne0  20235  rrgsupp  20634  abvne0  20752  gzrngunit  21388  chrnzr  21485  obsne0  21680  mdetdiaglem  22542  cnhaus  23298  hauscmplem  23350  fsubbas  23811  metn0  24304  nmne0  24563  nmgt0  24574  iccpnfhmeo  24899  ncvs1  25113  ipcau2  25190  dvcnvlem  25936  dvlip  25954  ftc1lem5  26003  mdegldg  26027  ply1divmo  26097  ig1peu  26136  ig1pdvds  26141  dgrmul  26232  coecj  26240  coecjOLD  26242  plydivlem4  26260  vieta1lem2  26275  vieta1  26276  aareccl  26290  geolim3  26303  abelthlem2  26398  abelthlem7  26404  tanregt0  26504  tanarg  26584  logtayl  26625  abscxp2  26658  cxpsqrt  26668  abscxpbnd  26719  logrec  26729  ang180lem1  26775  ang180lem2  26776  ang180lem3  26777  lawcos  26782  isosctr  26787  asinlem  26834  atandm2  26843  atandm4  26845  2efiatan  26884  tanatan  26885  atandmtan  26886  dvatan  26901  mersenne  27194  perfectlem2  27197  dchrinv  27228  dchrptlem2  27232  dchrsum2  27235  sumdchr2  27237  lgsabs1  27303  dchrisum0re  27480  ltsval2  27624  bday1  27810  cuteq1  27813  n0subs2  28360  tgcgrneq  28555  footexALT  28790  footexlem1  28791  footexlem2  28792  colinearalg  28983  axsegconlem6  28995  axsegconlem9  28998  ax5seglem5  29006  axlowdimlem14  29028  wlkn0  29694  cyclnspth  29874  iswwlksnx  29913  wwlksm1edg  29954  wspthsnonn0vne  29990  umgrclwwlkge2  30066  clwwisshclwws  30090  hashecclwwlkn1  30152  umgrhashecclwwlk  30153  frgrregord013  30470  frgrogt3nreg  30472  friendshipgt3  30473  nrt2irr  30548  nvgt0  30749  nv1  30750  nmlnogt0  30872  nmblolbii  30874  blocnilem  30879  normne0  31205  normcan  31651  nmlnopne0  32074  nmophmi  32106  riesz3i  32137  hashne0  32890  wrdpmtrlast  33175  cycpmco2lem6  33213  1arithidom  33618  ply1unit  33656  m1pmeq  33666  minplyirredlem  33867  constrrtcclem  33891  constrconj  33902  iconstr  33923  zarclssn  34030  esumpcvgval  34235  ballotlemfrcn0  34687  signsply0  34708  signstfvn  34726  signsvtn0  34727  signstfvneq0  34729  signstfveq0a  34733  signshnz  34748  bnj168  34886  nummin  35249  usgrgt2cycl  35324  erdszelem9  35393  segcon2  36299  outsideofeu  36325  heicant  37856  smprngopr  38253  isfldidl2  38270  isdmn3  38275  lsat0cv  39303  lcvexchlem1  39304  lsatcvat2  39321  lkrshp  39375  lkrshp3  39376  lkrpssN  39433  cvrat2  39699  atcvrneN  39700  atcvrj2b  39702  2llnmat  39794  2lnat  40054  pmapjat1  40123  pclfinclN  40220  lautlt  40361  ltrn11at  40417  ltrnatneq  40452  trlcone  40998  tendoconid  41099  tendotr  41100  cdleml3N  41248  dochsordN  41644  dochn0nv  41645  djhcvat42  41685  dochsatshp  41721  lcfl8b  41774  lclkrlem2a  41777  lcfrlem9  41820  mapdsord  41925  mapdncol  41940  mapdpglem29  41970  mapdindp1  41990  hdmapnzcl  42115  hdmaprnlem1N  42119  hdmaprnlem3N  42120  hdmaprnlem3uN  42121  hdmaprnlem9N  42127  hdmap14lem9  42146  hgmapval1  42163  hgmapadd  42164  hgmapmul  42165  hgmaprnlem1N  42166  hdmaplkr  42183  hdmapip1  42186  hgmapvvlem1  42193  hgmapvvlem2  42194  hgmapvvlem3  42195  fldhmf1  42354  aks6d1c2p2  42383  aks6d1c5lem2  42402  aks6d1c6lem3  42436  fsuppind  42843  jm2.19  43245  jm2.26lem3  43253  kelac1  43315  mpaaeu  43402  radcnvrat  44565  binomcxplemnotnn0  44607  sqrtnegnre  47563  paireqne  47767  fmtnoprmfac1lem  47820  requad01  47877  requad2  47879  perfectALTVlem2  47978  nnsgrpnmnd  48434  rrx2pnedifcoorneor  48972  rrx2pnedifcoorneorr  48973  eenglngeehlnmlem2  48994  fdomne0  49105  oppcendc  49273  onetansqsecsq  50016