Theorem necon3bid 2986

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

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

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 2942

This theorem is referenced by:  neeq1d  3001  neeq2d  3002  neeq12d  3003  nebi  3022  pr1nebg  4859  f1dom3fv3dif  7267  frxp  8112  frxp2  8130  frxp3  8137  suppval1  8152  iinon  8340  fodomfib  9326  wemapso  9546  wemapso2lem  9547  infpssrlem4  10301  ttukeylem6  10509  fodomb  10521  tskcard  10776  addneintrd  11421  addneintr2d  11422  negne0bd  11564  negned  11568  subne0d  11580  subne0ad  11582  subneintrd  11615  subneintr2d  11617  divne0b  11883  div2neg  11937  divne1d  12001  div2sub  12039  xaddass2  13229  xadddi2  13276  seqf1olem1  14007  expne0  14059  sqne0  14088  hashneq0  14324  hashnncl  14326  hashgt0  14348  ccat1st1st  14578  pfxn0  14636  cjne0  15110  recval  15269  absgt0  15271  abs1m  15282  abslem2  15286  sqreulem  15306  sqreu  15307  absne0d  15394  geoserg  15812  geolim  15816  geolim2  15817  georeclim  15818  geoisum1c  15826  tanval2  16076  tanaddlem  16109  tanadd  16110  4sqlem11  16888  ipodrsima  18494  f1omvdmvd  19311  f1omvdcnv  19312  f1omvdconj  19314  pmtrfmvdn0  19330  sylow1lem4  19469  dprdf1o  19902  dprd2da  19912  ringinvnz1ne0  20112  abvne0  20435  rrgsupp  20907  gzrngunit  21011  chrnzr  21082  obsne0  21280  mdetdiaglem  22100  cnhaus  22858  hauscmplem  22910  fsubbas  23371  metn0  23866  nmne0  24128  nmgt0  24139  iccpnfhmeo  24461  ncvs1  24674  ipcau2  24751  dvcnvlem  25493  dvlip  25510  ftc1lem5  25557  mdegldg  25584  ply1divmo  25653  ig1peu  25689  ig1pdvds  25694  dgrmul  25784  coecj  25792  plydivlem4  25809  vieta1lem2  25824  vieta1  25825  aareccl  25839  geolim3  25852  abelthlem2  25944  abelthlem7  25950  tanregt0  26048  tanarg  26127  logtayl  26168  abscxp2  26201  cxpsqrt  26211  abscxpbnd  26261  logrec  26268  ang180lem1  26314  ang180lem2  26315  ang180lem3  26316  lawcos  26321  isosctr  26326  asinlem  26373  atandm2  26382  atandm4  26384  2efiatan  26423  tanatan  26424  atandmtan  26425  dvatan  26440  mersenne  26730  perfectlem2  26733  dchrinv  26764  dchrptlem2  26768  dchrsum2  26771  sumdchr2  26773  lgsabs1  26839  dchrisum0re  27016  sltval2  27159  bday1s  27332  cuteq1  27334  tgcgrneq  27734  footexALT  27969  footexlem1  27970  footexlem2  27971  colinearalg  28168  axsegconlem6  28180  axsegconlem9  28183  ax5seglem5  28191  axlowdimlem14  28213  wlkn0  28878  cyclnspth  29057  iswwlksnx  29094  wwlksm1edg  29135  wspthsnonn0vne  29171  umgrclwwlkge2  29244  clwwisshclwws  29268  hashecclwwlkn1  29330  umgrhashecclwwlk  29331  frgrregord013  29648  frgrogt3nreg  29650  friendshipgt3  29651  nrt2irr  29726  nvgt0  29927  nv1  29928  nmlnogt0  30050  nmblolbii  30052  blocnilem  30057  normne0  30383  normcan  30829  nmlnopne0  31252  nmophmi  31284  riesz3i  31315  ogrpsublt  32239  cycpmco2lem6  32290  minplyirredlem  32769  zarclssn  32853  esumpcvgval  33076  ballotlemfrcn0  33528  signsply0  33562  signstfvn  33580  signsvtn0  33581  signstfvneq0  33583  signstfveq0a  33587  signshnz  33602  bnj168  33741  nummin  34094  usgrgt2cycl  34121  erdszelem9  34190  segcon2  35077  outsideofeu  35103  heicant  36523  smprngopr  36920  isfldidl2  36937  isdmn3  36942  lsat0cv  37903  lcvexchlem1  37904  lsatcvat2  37921  lkrshp  37975  lkrshp3  37976  lkrpssN  38033  cvrat2  38300  atcvrneN  38301  atcvrj2b  38303  2llnmat  38395  2lnat  38655  pmapjat1  38724  pclfinclN  38821  lautlt  38962  ltrn11at  39018  ltrnatneq  39053  trlcone  39599  tendoconid  39700  tendotr  39701  cdleml3N  39849  dochsordN  40245  dochn0nv  40246  djhcvat42  40286  dochsatshp  40322  lcfl8b  40375  lclkrlem2a  40378  lcfrlem9  40421  mapdsord  40526  mapdncol  40541  mapdpglem29  40571  mapdindp1  40591  hdmapnzcl  40716  hdmaprnlem1N  40720  hdmaprnlem3N  40721  hdmaprnlem3uN  40722  hdmaprnlem9N  40728  hdmap14lem9  40747  hgmapval1  40764  hgmapadd  40765  hgmapmul  40766  hgmaprnlem1N  40767  hdmaplkr  40784  hdmapip1  40787  hgmapvvlem1  40794  hgmapvvlem2  40795  hgmapvvlem3  40796  fldhmf1  40955  aks6d1c2p2  40957  fsuppind  41162  jm2.19  41732  jm2.26lem3  41740  kelac1  41805  mpaaeu  41892  radcnvrat  43073  binomcxplemnotnn0  43115  sqrtnegnre  46015  paireqne  46179  fmtnoprmfac1lem  46232  requad01  46289  requad2  46291  perfectALTVlem2  46390  nnsgrpnmnd  46588  rrx2pnedifcoorneor  47402  rrx2pnedifcoorneorr  47403  eenglngeehlnmlem2  47424  fdomne0  47516  onetansqsecsq  47806