MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon3bid Structured version   Visualization version   GIF version

Theorem necon3bid 2867
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
StepHypRef Expression
1 df-ne 2824 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon3bid.1 . . 3 (𝜑 → (𝐴 = 𝐵𝐶 = 𝐷))
32necon3bbid 2860 . 2 (𝜑 → (¬ 𝐴 = 𝐵𝐶𝐷))
41, 3syl5bb 272 1 (𝜑 → (𝐴𝐵𝐶𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196   = wceq 1523  wne 2823
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 197  df-ne 2824
This theorem is referenced by:  neeq1d  2882  neeq2d  2883  neeq12d  2884  nebi  2903  pr1nebg  4422  f1dom3fv3dif  6565  frxp  7332  suppval1  7346  iinon  7482  fodomfib  8281  wemapso  8497  wemapso2lem  8498  infpssrlem4  9166  ttukeylem6  9374  fodomb  9386  tskcard  9641  addneintrd  10281  addneintr2d  10282  negne0bd  10423  negned  10427  subne0d  10439  subne0ad  10441  subneintrd  10474  subneintr2d  10476  divne0b  10734  div2neg  10786  divne1d  10850  div2sub  10888  xaddass2  12118  xadddi2  12165  seqf1olem1  12880  expne0  12931  sqne0  12970  hashneq0  13193  hashnncl  13195  hashgt0  13215  swrdn0  13476  cjne0  13947  recval  14106  absgt0  14108  abs1m  14119  abslem2  14123  sqreulem  14143  sqreu  14144  absne0d  14230  geoserg  14642  geolim  14645  geolim2  14646  georeclim  14647  geoisum1c  14655  tanval2  14907  tanaddlem  14940  tanadd  14941  4sqlem11  15706  ipodrsima  17212  f1omvdmvd  17909  f1omvdcnv  17910  f1omvdconj  17912  pmtrfmvdn0  17928  sylow1lem4  18062  dprdf1o  18477  dprd2da  18487  ringinvnz1ne0  18638  abvne0  18875  rrgsupp  19339  gzrngunit  19860  chrnzr  19926  obsne0  20117  mdetdiaglem  20452  cnhaus  21206  hauscmplem  21257  fsubbas  21718  metn0  22212  nmne0  22470  nmgt0  22481  iccpnfhmeo  22791  ncvs1  23003  ipcau2  23079  dvcnvlem  23784  dvlip  23801  ftc1lem5  23848  mdegldg  23871  ply1divmo  23940  ig1peu  23976  ig1pdvds  23981  dgrmul  24071  coecj  24079  plydivlem4  24096  vieta1lem2  24111  vieta1  24112  aareccl  24126  geolim3  24139  abelthlem2  24231  abelthlem7  24237  tanregt0  24330  tanarg  24410  logtayl  24451  abscxp2  24484  cxpsqrt  24494  abscxpbnd  24539  logrec  24546  ang180lem1  24584  ang180lem2  24585  ang180lem3  24586  lawcos  24591  isosctr  24596  asinlem  24640  atandm2  24649  atandm4  24651  2efiatan  24690  tanatan  24691  atandmtan  24692  dvatan  24707  mersenne  24997  perfectlem2  25000  dchrinv  25031  dchrptlem2  25035  dchrsum2  25038  sumdchr2  25040  lgsabs1  25106  dchrisum0re  25247  tgcgrneq  25423  footex  25658  colinearalg  25835  axsegconlem6  25847  axsegconlem9  25850  ax5seglem5  25858  axlowdimlem14  25880  wlkn0  26572  cyclnspth  26751  iswwlksnx  26788  wwlksm1edg  26835  wspthsnonn0vne  26882  umgrclwwlkge2  26957  clwwisshclwws  26972  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  frgrregord013  27382  frgrogt3nreg  27384  friendshipgt3  27385  nvgt0  27657  nv1  27658  nmlnogt0  27780  nmblolbii  27782  blocnilem  27787  normne0  28115  normcan  28563  nmlnopne0  28986  nmophmi  29018  riesz3i  29049  ogrpsublt  29850  esumpcvgval  30268  ballotlemfrcn0  30719  signsply0  30756  signstfvn  30774  signsvtn0  30775  signstfvneq0  30777  signstfveq0a  30781  signshnz  30796  bnj168  30924  erdszelem9  31307  sltval2  31934  segcon2  32337  outsideofeu  32363  heicant  33574  smprngopr  33981  isfldidl2  33998  isdmn3  34003  lsat0cv  34638  lcvexchlem1  34639  lsatcvat2  34656  lkrshp  34710  lkrshp3  34711  lkrpssN  34768  cvrat2  35033  atcvrneN  35034  atcvrj2b  35036  2llnmat  35128  2lnat  35388  pmapjat1  35457  pclfinclN  35554  lautlt  35695  ltrn11at  35751  ltrnatneq  35787  trlcone  36333  tendoconid  36434  tendotr  36435  cdleml3N  36583  dochsordN  36980  dochn0nv  36981  djhcvat42  37021  dochsatshp  37057  lcfl8b  37110  lclkrlem2a  37113  lcfrlem9  37156  mapdsord  37261  mapdncol  37276  mapdpglem29  37306  mapdindp1  37326  hdmapnzcl  37454  hdmaprnlem1N  37458  hdmaprnlem3N  37459  hdmaprnlem3uN  37460  hdmaprnlem9N  37466  hdmap14lem9  37485  hgmapval1  37502  hgmapadd  37503  hgmapmul  37504  hgmaprnlem1N  37505  hdmaplkr  37522  hdmapip1  37525  hgmapvvlem1  37532  hgmapvvlem2  37533  hgmapvvlem3  37534  jm2.19  37877  jm2.26lem3  37885  kelac1  37950  mpaaeu  38037  radcnvrat  38830  binomcxplemnotnn0  38872  fmtnoprmfac1lem  41801  perfectALTVlem2  41956  nnsgrpnmnd  42143  onetansqsecsq  42830
  Copyright terms: Public domain W3C validator