Theorem necon3bid 2991

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

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

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 2947

This theorem is referenced by:  neeq1d  3006  neeq2d  3007  neeq12d  3008  nebi  3027  pr1nebg  4882  f1dom3fv3dif  7305  frxp  8167  frxp2  8185  frxp3  8192  suppval1  8207  iinon  8396  fodomfib  9397  fodomfibOLD  9399  wemapso  9620  wemapso2lem  9621  infpssrlem4  10375  ttukeylem6  10583  fodomb  10595  tskcard  10850  addneintrd  11497  addneintr2d  11498  negne0bd  11640  negned  11644  subne0d  11656  subne0ad  11658  subneintrd  11691  subneintr2d  11693  divne0b  11960  div2neg  12017  divne1d  12081  div2sub  12119  xaddass2  13312  xadddi2  13359  seqf1olem1  14092  expne0  14144  sqne0  14173  hashneq0  14413  hashnncl  14415  hashgt0  14437  ccat1st1st  14676  pfxn0  14734  cjne0  15212  recval  15371  absgt0  15373  abs1m  15384  abslem2  15388  sqreulem  15408  sqreu  15409  absne0d  15496  geoserg  15914  geolim  15918  geolim2  15919  georeclim  15920  geoisum1c  15928  tanval2  16181  tanaddlem  16214  tanadd  16215  4sqlem11  17002  ipodrsima  18611  f1omvdmvd  19485  f1omvdcnv  19486  f1omvdconj  19488  pmtrfmvdn0  19504  sylow1lem4  19643  dprdf1o  20076  dprd2da  20086  ringinvnz1ne0  20323  rrgsupp  20723  abvne0  20842  gzrngunit  21474  chrnzr  21568  obsne0  21768  mdetdiaglem  22625  cnhaus  23383  hauscmplem  23435  fsubbas  23896  metn0  24391  nmne0  24653  nmgt0  24664  iccpnfhmeo  24995  ncvs1  25210  ipcau2  25287  dvcnvlem  26034  dvlip  26052  ftc1lem5  26101  mdegldg  26125  ply1divmo  26195  ig1peu  26234  ig1pdvds  26239  dgrmul  26330  coecj  26338  plydivlem4  26356  vieta1lem2  26371  vieta1  26372  aareccl  26386  geolim3  26399  abelthlem2  26494  abelthlem7  26500  tanregt0  26599  tanarg  26679  logtayl  26720  abscxp2  26753  cxpsqrt  26763  abscxpbnd  26814  logrec  26824  ang180lem1  26870  ang180lem2  26871  ang180lem3  26872  lawcos  26877  isosctr  26882  asinlem  26929  atandm2  26938  atandm4  26940  2efiatan  26979  tanatan  26980  atandmtan  26981  dvatan  26996  mersenne  27289  perfectlem2  27292  dchrinv  27323  dchrptlem2  27327  dchrsum2  27330  sumdchr2  27332  lgsabs1  27398  dchrisum0re  27575  sltval2  27719  bday1s  27894  cuteq1  27896  tgcgrneq  28509  footexALT  28744  footexlem1  28745  footexlem2  28746  colinearalg  28943  axsegconlem6  28955  axsegconlem9  28958  ax5seglem5  28966  axlowdimlem14  28988  wlkn0  29657  cyclnspth  29836  iswwlksnx  29873  wwlksm1edg  29914  wspthsnonn0vne  29950  umgrclwwlkge2  30023  clwwisshclwws  30047  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  frgrregord013  30427  frgrogt3nreg  30429  friendshipgt3  30430  nrt2irr  30505  nvgt0  30706  nv1  30707  nmlnogt0  30829  nmblolbii  30831  blocnilem  30836  normne0  31162  normcan  31608  nmlnopne0  32031  nmophmi  32063  riesz3i  32094  chnind  32983  chnub  32984  ogrpsublt  33071  wrdpmtrlast  33086  cycpmco2lem6  33124  1arithidom  33530  ply1unit  33565  m1pmeq  33573  minplyirredlem  33703  constrrtcclem  33725  constrconj  33735  zarclssn  33819  esumpcvgval  34042  ballotlemfrcn0  34494  signsply0  34528  signstfvn  34546  signsvtn0  34547  signstfvneq0  34549  signstfveq0a  34553  signshnz  34568  bnj168  34706  nummin  35067  usgrgt2cycl  35098  erdszelem9  35167  segcon2  36069  outsideofeu  36095  heicant  37615  smprngopr  38012  isfldidl2  38029  isdmn3  38034  lsat0cv  38989  lcvexchlem1  38990  lsatcvat2  39007  lkrshp  39061  lkrshp3  39062  lkrpssN  39119  cvrat2  39386  atcvrneN  39387  atcvrj2b  39389  2llnmat  39481  2lnat  39741  pmapjat1  39810  pclfinclN  39907  lautlt  40048  ltrn11at  40104  ltrnatneq  40139  trlcone  40685  tendoconid  40786  tendotr  40787  cdleml3N  40935  dochsordN  41331  dochn0nv  41332  djhcvat42  41372  dochsatshp  41408  lcfl8b  41461  lclkrlem2a  41464  lcfrlem9  41507  mapdsord  41612  mapdncol  41627  mapdpglem29  41657  mapdindp1  41677  hdmapnzcl  41802  hdmaprnlem1N  41806  hdmaprnlem3N  41807  hdmaprnlem3uN  41808  hdmaprnlem9N  41814  hdmap14lem9  41833  hgmapval1  41850  hgmapadd  41851  hgmapmul  41852  hgmaprnlem1N  41853  hdmaplkr  41870  hdmapip1  41873  hgmapvvlem1  41880  hgmapvvlem2  41881  hgmapvvlem3  41882  fldhmf1  42047  aks6d1c2p2  42076  aks6d1c5lem2  42095  aks6d1c6lem3  42129  fsuppind  42545  jm2.19  42950  jm2.26lem3  42958  kelac1  43020  mpaaeu  43107  radcnvrat  44283  binomcxplemnotnn0  44325  sqrtnegnre  47222  paireqne  47385  fmtnoprmfac1lem  47438  requad01  47495  requad2  47497  perfectALTVlem2  47596  nnsgrpnmnd  47901  rrx2pnedifcoorneor  48450  rrx2pnedifcoorneorr  48451  eenglngeehlnmlem2  48472  fdomne0  48563  onetansqsecsq  48853