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

Theorem necon3bid 2826
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 2782 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon3bid.1 . . 3 (𝜑 → (𝐴 = 𝐵𝐶 = 𝐷))
32necon3bbid 2819 . 2 (𝜑 → (¬ 𝐴 = 𝐵𝐶𝐷))
41, 3syl5bb 271 1 (𝜑 → (𝐴𝐵𝐶𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195   = wceq 1475  wne 2780
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 196  df-ne 2782
This theorem is referenced by:  neeq1d  2841  neeq2d  2842  neeq12d  2843  nebi  2862  f1dom3fv3dif  6425  frxp  7174  suppval1  7188  iinon  7324  fodomfib  8125  wemapso  8339  wemapso2lem  8340  infpssrlem4  9011  ttukeylem6  9219  fodomb  9229  tskcard  9482  addneintrd  10122  addneintr2d  10123  negne0bd  10264  negned  10268  subne0d  10280  subne0ad  10282  subneintrd  10315  subneintr2d  10317  divne0b  10575  div2neg  10627  divne1d  10691  div2sub  10729  xaddass2  11952  xadddi2  11999  seqf1olem1  12702  expne0  12753  sqne0  12792  hashneq0  13016  hashnncl  13018  hashgt0  13038  swrdn0  13282  cjne0  13751  recval  13910  absgt0  13912  abs1m  13923  abslem2  13927  sqreulem  13947  sqreu  13948  absne0d  14034  geoserg  14437  geolim  14440  geolim2  14441  georeclim  14442  geoisum1c  14450  tanval2  14702  tanaddlem  14735  tanadd  14736  4sqlem11  15497  ipodrsima  16988  f1omvdmvd  17686  f1omvdcnv  17687  f1omvdconj  17689  pmtrfmvdn0  17705  sylow1lem4  17839  dprdf1o  18254  dprd2da  18264  ringinvnz1ne0  18415  abvne0  18650  rrgsupp  19112  gzrngunit  19631  chrnzr  19697  obsne0  19888  mdetdiaglem  20223  cnhaus  20968  hauscmplem  21019  fsubbas  21481  metn0  21975  nmne0  22233  nmgt0  22244  iccpnfhmeo  22552  ncvs1  22765  ipcau2  22841  dvcnvlem  23543  dvlip  23560  ftc1lem5  23607  mdegldg  23630  ply1divmo  23699  ig1peu  23735  ig1pdvds  23740  dgrmul  23830  coecj  23838  plydivlem4  23855  vieta1lem2  23870  vieta1  23871  aareccl  23885  geolim3  23898  abelthlem2  23990  abelthlem7  23996  tanregt0  24089  tanarg  24169  logtayl  24206  abscxp2  24239  cxpsqrt  24249  abscxpbnd  24294  logrec  24301  ang180lem1  24339  ang180lem2  24340  ang180lem3  24341  lawcos  24346  isosctr  24351  asinlem  24395  atandm2  24404  atandm4  24406  2efiatan  24445  tanatan  24446  atandmtan  24447  dvatan  24462  mersenne  24752  perfectlem2  24755  dchrinv  24786  dchrptlem2  24790  dchrsum2  24793  sumdchr2  24795  lgsabs1  24861  dchrisum0re  25002  tgcgrneq  25178  footex  25413  colinearalg  25590  axsegconlem6  25602  axsegconlem9  25605  ax5seglem5  25613  axlowdimlem14  25635  wlkn0  26055  wwlkn0s  26233  wwlkm1edg  26263  hashecclwwlkn1  26361  usghashecclwwlk  26362  frgrareg  26644  frgraregord013  26645  frgraregord13  26646  frgraogt3nreg  26647  friendshipgt3  26648  nvgt0  26913  nv1  26914  nmlnogt0  27036  nmblolbii  27038  blocnilem  27043  normne0  27371  normcan  27819  nmlnopne0  28242  nmophmi  28274  riesz3i  28305  ogrpsublt  29053  esumpcvgval  29467  ballotlemfrcn0  29918  signsply0  29954  signstfvn  29972  signsvtn0  29973  signstfvneq0  29975  signstfveq0a  29979  signshnz  29994  bnj168  30052  erdszelem9  30435  sltval2  31053  segcon2  31382  outsideofeu  31408  heicant  32614  smprngopr  33021  isfldidl2  33038  isdmn3  33043  lsat0cv  33338  lcvexchlem1  33339  lsatcvat2  33356  lkrshp  33410  lkrshp3  33411  lkrpssN  33468  cvrat2  33733  atcvrneN  33734  atcvrj2b  33736  2llnmat  33828  2lnat  34088  pmapjat1  34157  pclfinclN  34254  lautlt  34395  ltrn11at  34451  ltrnatneq  34487  trlcone  35034  tendoconid  35135  tendotr  35136  cdleml3N  35284  dochsordN  35681  dochn0nv  35682  djhcvat42  35722  dochsatshp  35758  lcfl8b  35811  lclkrlem2a  35814  lcfrlem9  35857  mapdsord  35962  mapdncol  35977  mapdpglem29  36007  mapdindp1  36027  hdmapnzcl  36155  hdmaprnlem1N  36159  hdmaprnlem3N  36160  hdmaprnlem3uN  36161  hdmaprnlem9N  36167  hdmap14lem9  36186  hgmapval1  36203  hgmapadd  36204  hgmapmul  36205  hgmaprnlem1N  36206  hdmaplkr  36223  hdmapip1  36226  hgmapvvlem1  36233  hgmapvvlem2  36234  hgmapvvlem3  36235  jm2.19  36578  jm2.26lem3  36586  kelac1  36651  mpaaeu  36739  radcnvrat  37535  binomcxplemnotnn0  37577  fmtnoprmfac1lem  40014  perfectALTVlem2  40165  pr1nebg  40314  1wlkn0  40825  cyclnsPth  41006  iswwlksnx  41042  wwlksm1edg  41078  wspthsnonn0vne  41124  isclwwlksnx  41197  umgrclwwlksge2  41219  clwwisshclwws  41235  hashecclwwlksn1  41261  umgrhashecclwwlk  41262  av-frgraregord013  41549  av-frgraogt3nreg  41551  av-friendshipgt3  41552  nnsgrpnmnd  41608  onetansqsecsq  42301
  Copyright terms: Public domain W3C validator