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

Theorem necon3bid 3051
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 3008 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon3bid.1 . . 3 (𝜑 → (𝐴 = 𝐵𝐶 = 𝐷))
32necon3bbid 3044 . 2 (𝜑 → (¬ 𝐴 = 𝐵𝐶𝐷))
41, 3syl5bb 286 1 (𝜑 → (𝐴𝐵𝐶𝐷))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209   = wceq 1538  wne 3007
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 210  df-ne 3008
This theorem is referenced by:  neeq1d  3066  neeq2d  3067  neeq12d  3068  nebi  3087  pr1nebg  4761  f1dom3fv3dif  7000  frxp  7795  suppval1  7811  iinon  7952  fodomfib  8774  wemapso  8991  wemapso2lem  8992  infpssrlem4  9705  ttukeylem6  9913  fodomb  9925  tskcard  10180  addneintrd  10824  addneintr2d  10825  negne0bd  10967  negned  10971  subne0d  10983  subne0ad  10985  subneintrd  11018  subneintr2d  11020  divne0b  11286  div2neg  11340  divne1d  11404  div2sub  11442  xaddass2  12621  xadddi2  12668  seqf1olem1  13393  expne0  13444  sqne0  13473  hashneq0  13709  hashnncl  13711  hashgt0  13733  ccat1st1st  13963  pfxn0  14027  cjne0  14501  recval  14661  absgt0  14663  abs1m  14674  abslem2  14678  sqreulem  14698  sqreu  14699  absne0d  14786  geoserg  15200  geolim  15205  geolim2  15206  georeclim  15207  geoisum1c  15215  tanval2  15465  tanaddlem  15498  tanadd  15499  4sqlem11  16268  ipodrsima  17754  f1omvdmvd  18550  f1omvdcnv  18551  f1omvdconj  18553  pmtrfmvdn0  18569  sylow1lem4  18705  dprdf1o  19133  dprd2da  19143  ringinvnz1ne0  19321  abvne0  19574  rrgsupp  20040  mhpinvcl  20315  gzrngunit  20587  chrnzr  20653  obsne0  20845  mdetdiaglem  21183  cnhaus  21938  hauscmplem  21990  fsubbas  22451  metn0  22946  nmne0  23204  nmgt0  23215  iccpnfhmeo  23529  ncvs1  23741  ipcau2  23817  dvcnvlem  24558  dvlip  24575  ftc1lem5  24622  mdegldg  24646  ply1divmo  24715  ig1peu  24751  ig1pdvds  24756  dgrmul  24846  coecj  24854  plydivlem4  24871  vieta1lem2  24886  vieta1  24887  aareccl  24901  geolim3  24914  abelthlem2  25006  abelthlem7  25012  tanregt0  25110  tanarg  25189  logtayl  25230  abscxp2  25263  cxpsqrt  25273  abscxpbnd  25321  logrec  25328  ang180lem1  25374  ang180lem2  25375  ang180lem3  25376  lawcos  25381  isosctr  25386  asinlem  25433  atandm2  25442  atandm4  25444  2efiatan  25483  tanatan  25484  atandmtan  25485  dvatan  25500  mersenne  25790  perfectlem2  25793  dchrinv  25824  dchrptlem2  25828  dchrsum2  25831  sumdchr2  25833  lgsabs1  25899  dchrisum0re  26076  tgcgrneq  26256  footexALT  26491  footexlem1  26492  footexlem2  26493  colinearalg  26683  axsegconlem6  26695  axsegconlem9  26698  ax5seglem5  26706  axlowdimlem14  26728  wlkn0  27389  cyclnspth  27568  iswwlksnx  27605  wwlksm1edg  27646  wspthsnonn0vne  27682  umgrclwwlkge2  27755  clwwisshclwws  27779  hashecclwwlkn1  27841  umgrhashecclwwlk  27842  frgrregord013  28159  frgrogt3nreg  28161  friendshipgt3  28162  nvgt0  28436  nv1  28437  nmlnogt0  28559  nmblolbii  28561  blocnilem  28566  normne0  28892  normcan  29338  nmlnopne0  29761  nmophmi  29793  riesz3i  29824  ogrpsublt  30730  cycpmco2lem6  30781  esumpcvgval  31345  ballotlemfrcn0  31795  signsply0  31829  signstfvn  31847  signsvtn0  31848  signstfvneq0  31850  signstfveq0a  31854  signshnz  31869  bnj168  32008  usgrgt2cycl  32385  erdszelem9  32454  sltval2  33171  segcon2  33574  outsideofeu  33600  heicant  34978  smprngopr  35376  isfldidl2  35393  isdmn3  35398  lsat0cv  36215  lcvexchlem1  36216  lsatcvat2  36233  lkrshp  36287  lkrshp3  36288  lkrpssN  36345  cvrat2  36611  atcvrneN  36612  atcvrj2b  36614  2llnmat  36706  2lnat  36966  pmapjat1  37035  pclfinclN  37132  lautlt  37273  ltrn11at  37329  ltrnatneq  37364  trlcone  37910  tendoconid  38011  tendotr  38012  cdleml3N  38160  dochsordN  38556  dochn0nv  38557  djhcvat42  38597  dochsatshp  38633  lcfl8b  38686  lclkrlem2a  38689  lcfrlem9  38732  mapdsord  38837  mapdncol  38852  mapdpglem29  38882  mapdindp1  38902  hdmapnzcl  39027  hdmaprnlem1N  39031  hdmaprnlem3N  39032  hdmaprnlem3uN  39033  hdmaprnlem9N  39039  hdmap14lem9  39058  hgmapval1  39075  hgmapadd  39076  hgmapmul  39077  hgmaprnlem1N  39078  hdmaplkr  39095  hdmapip1  39098  hgmapvvlem1  39105  hgmapvvlem2  39106  hgmapvvlem3  39107  jm2.19  39745  jm2.26lem3  39753  kelac1  39818  mpaaeu  39905  radcnvrat  40833  binomcxplemnotnn0  40875  sqrtnegnre  43687  paireqne  43851  fmtnoprmfac1lem  43904  requad01  43962  requad2  43964  perfectALTVlem2  44063  nnsgrpnmnd  44261  rrx2pnedifcoorneor  44941  rrx2pnedifcoorneorr  44942  eenglngeehlnmlem2  44963  onetansqsecsq  45098
  Copyright terms: Public domain W3C validator