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

Theorem neneqd 2828
Description: Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
neneqd.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
neneqd (𝜑 → ¬ 𝐴 = 𝐵)

Proof of Theorem neneqd
StepHypRef Expression
1 neneqd.1 . 2 (𝜑𝐴𝐵)
2 df-ne 2824 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2sylib 208 1 (𝜑 → ¬ 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = 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:  neneq  2829  necon2bi  2853  necon2i  2857  necon4i  2858  pm2.21ddne  2907  nelrdva  3450  disjprg  4680  0inp0  4867  onnseq  7486  sniffsupp  8356  ackbij1lem15  9094  ttukeylem7  9375  fpwwe2lem13  9502  canthnumlem  9508  canthp1lem2  9513  recgt0  10905  elnnz  11425  xrnemnf  11989  xrnepnf  11990  fzprval  12439  fzodisjsn  12545  expnnval  12903  elprchashprn2  13222  relexpsucnnr  13809  relexp1g  13810  relexpuzrel  13836  sgnp  13874  fprodn0f  14766  ruclem12  15014  dvdsle  15079  nndvdslegcd  15274  gcdnncl  15276  divgcdnn  15283  sqgcd  15325  eucalgf  15343  eucalginv  15344  lcmgcdlem  15366  lcmftp  15396  lcmfunsnlem2lem1  15398  lcmfunsnlem2lem2  15399  qredeu  15419  rpdvds  15421  cncongr2  15429  divnumden  15503  divdenle  15504  phisum  15542  oddprm  15562  pythagtriplem4  15571  pythagtriplem8  15575  pythagtriplem9  15576  pythagtriplem19  15585  4sqlem10  15698  ram0  15773  isipodrs  17208  gsumval2  17327  mulgnn  17594  sylow1lem1  18059  gsumval3eu  18351  abvtrivd  18888  00lss  18990  lvecvscan2  19160  fidomndrng  19355  mvrcl  19497  mplmon  19511  mplmonmul  19512  evlslem3  19562  coe1tmfv2  19693  cply1coe0  19717  cply1coe0bi  19718  prmirredlem  19889  uvcff  20178  1marepvsma1  20437  mdetrsca2  20458  mdetrlin2  20461  mdetunilem2  20467  mdetunilem5  20470  mdetunilem6  20471  mdetunilem9  20474  maducoeval2  20494  gsummatr01lem3  20511  gsummatr01lem4  20512  gsummatr01  20513  m2cpm  20594  m2cpminvid2lem  20607  fvmptnn04ifa  20703  fvmptnn04ifb  20704  fvmptnn04ifc  20705  chfacffsupp  20709  chfacfscmul0  20711  chfacfscmulgsum  20713  chfacfpmmul0  20715  chfacfpmmulgsum  20717  connclo  21266  dissnlocfin  21380  ptpjpre2  21431  txindis  21485  snfil  21715  alexsublem  21895  tsmsfbas  21978  stdbdxmet  22367  dscmet  22424  xrsxmet  22659  iccpnfcnv  22790  cphsubrglem  23023  minveclem3b  23245  minveclem4a  23247  ovolicc1  23330  dvexp2  23762  dvmptdiv  23782  lhop2  23823  deg1sublt  23915  ig1pval3  23979  dvply1  24084  plydiveu  24098  quotcan  24109  aaliou3lem9  24150  taylthlem2  24173  pserdvlem2  24227  abelthlem9  24239  logccne0  24370  logtayllem  24450  logtayl  24451  cxpef  24456  angrtmuld  24583  isosctrlem2  24594  isosctrlem3  24595  chordthmlem  24604  leibpilem2  24713  leibpi  24714  rlimcnp2  24738  efrlim  24741  vma1  24937  muinv  24964  lgsval2lem  25077  lgsval4  25087  lgsdir  25102  lgseisenlem4  25148  lgsquadlem1  25150  lgsquad2  25156  m1lgs  25158  2sqlem8a  25195  2sqlem8  25196  padicabv  25364  ostth1  25367  ostth3  25372  tgbtwnne  25430  tgbtwndiff  25446  tgcolg  25494  tgbtwnconn1lem3  25514  legso  25539  tglineeltr  25571  tglineintmo  25582  tglineneq  25584  colline  25589  mirne  25607  miriso  25610  mirhl  25619  mirbtwnhl  25620  symquadlem  25629  krippenlem  25630  midexlem  25632  ragncol  25649  footex  25658  colperp  25666  colperpexlem3  25669  mideulem2  25671  opphllem  25672  midex  25674  opptgdim2  25682  oppperpex  25690  hlpasch  25693  colopp  25706  colhp  25707  lmieu  25721  trgcopy  25741  cgracol  25764  cgrg3col4  25779  axlowdimlem15  25881  axcontlem2  25890  axcontlem7  25895  1egrvtxdg0  26463  2pthnloop  26683  cyclnspth  26751  eupth2lem1  27196  eupth2lem2  27197  eupth2lem3lem6  27211  strlem6  29243  hstrlem6  29251  atssma  29365  chirredlem1  29377  znsqcld  29640  xaddeq0  29646  xlt2addrd  29651  divnumden2  29692  2sqcoprm  29775  2sqmod  29776  submomnd  29838  ornglmullt  29935  orngrmullt  29936  ofldchr  29942  suborng  29943  pmtridf1o  29984  pmtridfv1  29985  pmtridfv2  29986  1smat1  29998  submatminr1  30004  madjusmdetlem2  30022  xrge0iifcnv  30107  xrge0iifcv  30108  xrge0iif1  30112  qqhval2lem  30153  qqhf  30158  qqhre  30192  esumrnmpt2  30258  esumcvgre  30281  inelpisys  30345  carsgclctunlem2  30509  ballotlemirc  30721  sgnmul  30732  sgn0bi  30737  signswlid  30764  repr0  30817  reprlt  30825  reprgt  30827  reprinfz1  30828  tgoldbachgtda  30867  tgoldbachgt  30869  bnj1523  31265  fz0n  31742  dfrdg2  31825  nolesgn2ores  31950  nosep1o  31957  nosepdmlem  31958  nosepssdm  31961  noresle  31971  nosupbnd1lem3  31981  nosupbnd1lem4  31982  nosupbnd1lem5  31983  nosupbnd1lem6  31984  nosupbnd2lem1  31986  dfrdg4  32183  broutsideof2  32354  outsidele  32364  rankeq1o  32403  ivthALT  32455  limsucncmpi  32569  topdifinffinlem  33325  icorempt2  33329  finxpreclem2  33357  finxp1o  33359  finxpreclem6  33363  poimirlem9  33548  poimirlem11  33550  poimirlem12  33551  poimirlem25  33564  fdc  33671  heibor1lem  33738  heiborlem4  33743  heiborlem6  33745  2atm  35131  lhpocnle  35620  lhp2at0nle  35639  trlval3  35792  cdleme18c  35898  cdlemg17b  36267  cdlemg17i  36274  dia2dimlem2  36671  dia2dimlem3  36672  dihord6apre  36862  dihatlat  36940  dochshpsat  37060  lcfrlem9  37156  mapdhval2  37332  hdmap1val2  37407  hdmap14lem4a  37480  hdmap14lem6  37482  jm2.26lem3  37885  kelac1  37950  clsk3nimkb  38655  clsk1indlem0  38656  sineq0ALT  39487  refsum2cnlem1  39510  disjxp1  39552  nelrnmpt  39571  disjf1  39683  disjrnmpt2  39689  disjinfi  39694  rnmptn0  39727  oddfl  39803  xrlttri5d  39809  supxrge  39867  nepnfltpnf  39871  nemnftgtmnft  39873  xrlexaddrp  39881  xrred  39894  supminfxr2  40012  icoiccdif  40068  qinioo  40080  ioonct  40082  fmul01lt1lem1  40134  climrec  40153  limcperiod  40178  reclimc  40203  limsupub  40254  cncfiooicclem1  40424  cncfioobdlem  40427  fperdvper  40451  dvdivbd  40456  ditgeqiooicc  40494  itgsincmulx  40508  itgioocnicc  40511  iblcncfioo  40512  stoweidlem35  40570  stoweidlem39  40574  stirlinglem5  40613  stirlinglem8  40616  dirkerper  40631  dirkercncflem2  40639  dirkercncflem4  40641  fourierdlem31  40673  fourierdlem34  40676  fourierdlem41  40683  fourierdlem42  40684  fourierdlem44  40686  fourierdlem48  40689  fourierdlem49  40690  fourierdlem53  40694  fourierdlem56  40697  fourierdlem58  40699  fourierdlem60  40701  fourierdlem61  40702  fourierdlem62  40703  fourierdlem65  40706  fourierdlem66  40707  fourierdlem73  40714  fourierdlem76  40717  fourierdlem79  40720  fourierdlem81  40722  fourierdlem82  40723  fourierdlem93  40734  fourierdlem103  40744  fourierdlem104  40745  sqwvfoura  40763  fourierswlem  40765  elaa2lem  40768  elaa2  40769  etransclem4  40773  etransclem24  40793  etransclem31  40800  etransclem32  40801  etransclem35  40804  sge0repnf  40921  sge0fodjrnlem  40951  sge0iunmpt  40953  sge0rpcpnf  40956  nnfoctbdjlem  40990  meadjun  40997  voliunsge0lem  41007  hoicvr  41083  ovnn0val  41086  ovnsubaddlem1  41105  hoidmvn0val  41119  hsphoidmvle  41121  hoidmv1lelem1  41126  hoidmv1lelem2  41127  hoidmv1lelem3  41128  ovnhoilem1  41136  ovnsubadd2lem  41180  ovnovollem3  41193  lighneallem3  41849  divgcdoddALTV  41918  dignn0flhalflem1  42734
  Copyright terms: Public domain W3C validator