Theorem necon3bid 3001

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   = wceq 1560   ≠ wne 2957

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 209  df-ne 2958

This theorem is referenced by:  neeq1d  3016  neeq2d  3017  neeq12d  3018  nebi  3037  pr1nebg  4816  f1dom3fv3dif  7252  frxp  8106  frxp2  8124  frxp3  8131  suppval1  8146  iinon  8311  fodomfib  9273  fodomfibOLD  9274  wemapso  9499  wemapso2lem  9500  infpssrlem4  10263  ttukeylem6  10471  fodomb  10483  tskcard  10739  addneintrd  11390  addneintr2d  11391  negne0bd  11535  negned  11539  subne0d  11551  subne0ad  11553  subneintrd  11586  subneintr2d  11588  divne0b  11856  div2neg  11914  divne1d  11978  div2sub  12016  xaddass2  13253  xadddi2  13300  seqf1olem1  14054  expne0  14106  sqne0  14136  hashneq0  14377  hashnncl  14379  hashgt0  14401  ccat1st1st  14642  pfxn0  14700  cjne0  15190  recval  15350  absgt0  15352  abs1m  15363  abslem2  15367  sqreulem  15387  sqreu  15388  absne0d  15477  geoserg  15896  geolim  15900  geolim2  15901  georeclim  15902  geoisum1c  15910  tanval2  16165  tanaddlem  16198  tanadd  16199  4sqlem11  16991  ipodrsima  18573  chnind  18653  chnub  18654  f1omvdmvd  19483  f1omvdcnv  19484  f1omvdconj  19486  pmtrfmvdn0  19502  sylow1lem4  19641  dprdf1o  20074  dprd2da  20084  ogrpsublt  20182  ringinvnz1ne0  20350  rrgsupp  20751  abvne0  20868  gzrngunit  21485  chrnzr  21582  obsne0  21777  mdetdiaglem  22658  cnhaus  23414  hauscmplem  23466  fsubbas  23927  metn0  24420  nmne0  24679  nmgt0  24690  iccpnfhmeo  25007  ncvs1  25219  ipcau2  25296  dvcnvlem  26038  dvlip  26055  ftc1lem5  26102  mdegldg  26126  ply1divmo  26196  ig1peu  26235  ig1pdvds  26240  dgrmul  26330  coecj  26338  coecjOLD  26340  plydivlem4  26360  vieta1lem2  26375  vieta1  26376  aareccl  26390  geolim3  26403  abelthlem2  26495  abelthlem7  26501  tanregt0  26604  tanarg  26684  logtayl  26725  abscxp2  26758  cxpsqrt  26768  abscxpbnd  26818  logrec  26828  ang180lem1  26874  ang180lem2  26875  ang180lem3  26876  lawcos  26881  isosctr  26886  asinlem  26933  atandm2  26942  atandm4  26944  2efiatan  26983  tanatan  26984  atandmtan  26985  dvatan  27000  mersenne  27291  perfectlem2  27294  dchrinv  27325  dchrptlem2  27329  dchrsum2  27332  sumdchr2  27334  lgsabs1  27400  dchrisum0re  27577  ltsval2  27720  bday1  27907  cuteq1  27910  n0subs2  28457  tgcgrneq  28652  footexALT  28891  footexlem1  28892  footexlem2  28893  colinearalg  29111  axsegconlem6  29123  axsegconlem9  29126  ax5seglem5  29134  axlowdimlem14  29156  wlkn0  29821  cyclnspth  30001  iswwlksnx  30040  wwlksm1edg  30081  wspthsnonn0vne  30117  umgrclwwlkge2  30193  clwwisshclwws  30217  hashecclwwlkn1  30279  umgrhashecclwwlk  30280  frgrregord013  30597  frgrogt3nreg  30599  friendshipgt3  30600  nrt2irr  30675  nvgt0  30877  nv1  30878  nmlnogt0  31000  nmblolbii  31002  blocnilem  31007  normne0  31333  normcan  31779  nmlnopne0  32202  nmophmi  32234  riesz3i  32265  hashne0  33012  wrdpmtrlast  33273  cycpmco2lem6  33311  1arithidom  33733  ply1unit  33771  m1pmeq  33781  minplyirredlem  34007  constrrtcclem  34031  constrconj  34042  iconstr  34063  zarclssn  34170  esumpcvgval  34375  ballotlemfrcn0  34827  signsply0  34845  signstfvn  34863  signsvtn0  34864  signstfvneq0  34866  signstfveq0a  34870  signshnz  34885  bnj168  35026  nummin  35389  usgrgt2cycl  35480  erdszelem9  35549  segcon2  36455  outsideofeu  36481  heicant  38154  smprngopr  38551  isfldidl2  38568  isdmn3  38573  lsat0cv  39657  lcvexchlem1  39658  lsatcvat2  39675  lkrshp  39729  lkrshp3  39730  lkrpssN  39787  cvrat2  40053  atcvrneN  40054  atcvrj2b  40056  2llnmat  40148  2lnat  40408  pmapjat1  40477  pclfinclN  40574  lautlt  40715  ltrn11at  40771  ltrnatneq  40806  trlcone  41352  tendoconid  41453  tendotr  41454  cdleml3N  41602  dochsordN  41998  dochn0nv  41999  djhcvat42  42039  dochsatshp  42075  lcfl8b  42128  lclkrlem2a  42131  lcfrlem9  42174  mapdsord  42279  mapdncol  42294  mapdpglem29  42324  mapdindp1  42344  hdmapnzcl  42469  hdmaprnlem1N  42473  hdmaprnlem3N  42474  hdmaprnlem3uN  42475  hdmaprnlem9N  42481  hdmap14lem9  42500  hgmapval1  42517  hgmapadd  42518  hgmapmul  42519  hgmaprnlem1N  42520  hdmaplkr  42537  hdmapip1  42540  hgmapvvlem1  42547  hgmapvvlem2  42548  hgmapvvlem3  42549  fldhmf1  42707  aks6d1c2p2  42736  aks6d1c5lem2  42755  aks6d1c6lem3  42789  redivne0bd  43059  fsuppind  43172  jm2.19  43570  jm2.26lem3  43578  kelac1  43640  mpaaeu  43727  radcnvrat  44890  binomcxplemnotnn0  44932  sqrtnegnre  47901  paireqne  48117  fmtnoprmfac1lem  48173  requad01  48243  requad2  48245  perfectALTVlem2  48344  nnsgrpnmnd  48800  rrx2pnedifcoorneor  49338  rrx2pnedifcoorneorr  49339  eenglngeehlnmlem2  49360  fdomne0  49471  oppcendc  49639  onetansqsecsq  50382