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 1540   ≠ 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  4834  f1dom3fv3dif  7261  frxp  8125  frxp2  8143  frxp3  8150  suppval1  8165  iinon  8354  fodomfib  9341  fodomfibOLD  9343  wemapso  9565  wemapso2lem  9566  infpssrlem4  10320  ttukeylem6  10528  fodomb  10540  tskcard  10795  addneintrd  11442  addneintr2d  11443  negne0bd  11587  negned  11591  subne0d  11603  subne0ad  11605  subneintrd  11638  subneintr2d  11640  divne0b  11907  div2neg  11964  divne1d  12028  div2sub  12066  xaddass2  13266  xadddi2  13313  seqf1olem1  14059  expne0  14111  sqne0  14141  hashneq0  14382  hashnncl  14384  hashgt0  14406  ccat1st1st  14646  pfxn0  14704  cjne0  15182  recval  15341  absgt0  15343  abs1m  15354  abslem2  15358  sqreulem  15378  sqreu  15379  absne0d  15466  geoserg  15882  geolim  15886  geolim2  15887  georeclim  15888  geoisum1c  15896  tanval2  16151  tanaddlem  16184  tanadd  16185  4sqlem11  16975  ipodrsima  18551  f1omvdmvd  19424  f1omvdcnv  19425  f1omvdconj  19427  pmtrfmvdn0  19443  sylow1lem4  19582  dprdf1o  20015  dprd2da  20025  ringinvnz1ne0  20260  rrgsupp  20661  abvne0  20779  gzrngunit  21401  chrnzr  21491  obsne0  21685  mdetdiaglem  22536  cnhaus  23292  hauscmplem  23344  fsubbas  23805  metn0  24299  nmne0  24558  nmgt0  24569  iccpnfhmeo  24894  ncvs1  25109  ipcau2  25186  dvcnvlem  25932  dvlip  25950  ftc1lem5  25999  mdegldg  26023  ply1divmo  26093  ig1peu  26132  ig1pdvds  26137  dgrmul  26228  coecj  26236  coecjOLD  26238  plydivlem4  26256  vieta1lem2  26271  vieta1  26272  aareccl  26286  geolim3  26299  abelthlem2  26394  abelthlem7  26400  tanregt0  26500  tanarg  26580  logtayl  26621  abscxp2  26654  cxpsqrt  26664  abscxpbnd  26715  logrec  26725  ang180lem1  26771  ang180lem2  26772  ang180lem3  26773  lawcos  26778  isosctr  26783  asinlem  26830  atandm2  26839  atandm4  26841  2efiatan  26880  tanatan  26881  atandmtan  26882  dvatan  26897  mersenne  27190  perfectlem2  27193  dchrinv  27224  dchrptlem2  27228  dchrsum2  27231  sumdchr2  27233  lgsabs1  27299  dchrisum0re  27476  sltval2  27620  bday1s  27795  cuteq1  27798  n0subs2  28306  tgcgrneq  28462  footexALT  28697  footexlem1  28698  footexlem2  28699  colinearalg  28889  axsegconlem6  28901  axsegconlem9  28904  ax5seglem5  28912  axlowdimlem14  28934  wlkn0  29601  cyclnspth  29783  iswwlksnx  29822  wwlksm1edg  29863  wspthsnonn0vne  29899  umgrclwwlkge2  29972  clwwisshclwws  29996  hashecclwwlkn1  30058  umgrhashecclwwlk  30059  frgrregord013  30376  frgrogt3nreg  30378  friendshipgt3  30379  nrt2irr  30454  nvgt0  30655  nv1  30656  nmlnogt0  30778  nmblolbii  30780  blocnilem  30785  normne0  31111  normcan  31557  nmlnopne0  31980  nmophmi  32012  riesz3i  32043  hashne0  32789  chnind  32991  chnub  32992  ogrpsublt  33089  wrdpmtrlast  33104  cycpmco2lem6  33142  1arithidom  33552  ply1unit  33588  m1pmeq  33596  minplyirredlem  33744  constrrtcclem  33768  constrconj  33779  iconstr  33800  zarclssn  33904  esumpcvgval  34109  ballotlemfrcn0  34562  signsply0  34583  signstfvn  34601  signsvtn0  34602  signstfvneq0  34604  signstfveq0a  34608  signshnz  34623  bnj168  34761  nummin  35122  usgrgt2cycl  35152  erdszelem9  35221  segcon2  36123  outsideofeu  36149  heicant  37679  smprngopr  38076  isfldidl2  38093  isdmn3  38098  lsat0cv  39051  lcvexchlem1  39052  lsatcvat2  39069  lkrshp  39123  lkrshp3  39124  lkrpssN  39181  cvrat2  39448  atcvrneN  39449  atcvrj2b  39451  2llnmat  39543  2lnat  39803  pmapjat1  39872  pclfinclN  39969  lautlt  40110  ltrn11at  40166  ltrnatneq  40201  trlcone  40747  tendoconid  40848  tendotr  40849  cdleml3N  40997  dochsordN  41393  dochn0nv  41394  djhcvat42  41434  dochsatshp  41470  lcfl8b  41523  lclkrlem2a  41526  lcfrlem9  41569  mapdsord  41674  mapdncol  41689  mapdpglem29  41719  mapdindp1  41739  hdmapnzcl  41864  hdmaprnlem1N  41868  hdmaprnlem3N  41869  hdmaprnlem3uN  41870  hdmaprnlem9N  41876  hdmap14lem9  41895  hgmapval1  41912  hgmapadd  41913  hgmapmul  41914  hgmaprnlem1N  41915  hdmaplkr  41932  hdmapip1  41935  hgmapvvlem1  41942  hgmapvvlem2  41943  hgmapvvlem3  41944  fldhmf1  42103  aks6d1c2p2  42132  aks6d1c5lem2  42151  aks6d1c6lem3  42185  fsuppind  42613  jm2.19  43017  jm2.26lem3  43025  kelac1  43087  mpaaeu  43174  radcnvrat  44338  binomcxplemnotnn0  44380  sqrtnegnre  47336  paireqne  47525  fmtnoprmfac1lem  47578  requad01  47635  requad2  47637  perfectALTVlem2  47736  nnsgrpnmnd  48153  rrx2pnedifcoorneor  48696  rrx2pnedifcoorneorr  48697  eenglngeehlnmlem2  48718  fdomne0  48828  oppcendc  48993  onetansqsecsq  49625