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

Theorem neneqd 2983
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 2979 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2sylib 209 1 (𝜑 → ¬ 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1637  wne 2978
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 198  df-ne 2979
This theorem is referenced by:  neneq  2984  necon2bi  3008  necon2i  3012  necon4i  3013  pm2.21ddne  3062  nelrdva  3615  disjprg  4840  0inp0  5029  onnseq  7673  sniffsupp  8550  dfac2b  9232  ackbij1lem15  9337  ttukeylem7  9618  fpwwe2lem13  9745  canthnumlem  9751  canthp1lem2  9756  recgt0  11148  elnnz  11649  xrnemnf  12163  xrnepnf  12164  fzprval  12620  fzodisjsn  12726  expnnval  13082  elprchashprn2  13397  relexpsucnnr  13984  relexp1g  13985  relexpuzrel  14011  sgnp  14049  fprodn0f  14938  ruclem12  15186  dvdsle  15251  nndvdslegcd  15442  gcdnncl  15444  divgcdnn  15451  sqgcd  15493  eucalgf  15511  eucalginv  15512  lcmgcdlem  15534  lcmftp  15564  lcmfunsnlem2lem1  15566  lcmfunsnlem2lem2  15567  qredeu  15586  rpdvds  15588  cncongr2  15596  divnumden  15669  divdenle  15670  phisum  15708  oddprm  15728  pythagtriplem4  15737  pythagtriplem8  15741  pythagtriplem9  15742  pythagtriplem19  15751  4sqlem10  15864  ram0  15939  isipodrs  17362  gsumval2  17481  mulgnn  17748  sylow1lem1  18210  gsumval3eu  18502  abvtrivd  19040  00lss  19142  lvecvscan2  19315  fidomndrng  19512  mvrcl  19654  mplmon  19668  mplmonmul  19669  evlslem3  19718  coe1tmfv2  19849  cply1coe0  19873  cply1coe0bi  19874  prmirredlem  20045  uvcff  20337  1marepvsma1  20597  mdetrsca2  20618  mdetrlin2  20621  mdetunilem2  20627  mdetunilem5  20630  mdetunilem6  20631  mdetunilem9  20634  maducoeval2  20654  gsummatr01lem3  20672  gsummatr01lem4  20673  gsummatr01  20674  m2cpm  20756  m2cpminvid2lem  20769  fvmptnn04ifa  20865  fvmptnn04ifb  20866  fvmptnn04ifc  20867  chfacffsupp  20871  chfacfscmul0  20873  chfacfscmulgsum  20875  chfacfpmmul0  20877  chfacfpmmulgsum  20879  connclo  21429  dissnlocfin  21543  ptpjpre2  21594  txindis  21648  snfil  21878  alexsublem  22058  tsmsfbas  22141  stdbdxmet  22530  dscmet  22587  xrsxmet  22822  iccpnfcnv  22953  cphsubrglem  23186  minveclem3b  23410  minveclem4a  23412  ovolicc1  23496  dvexp2  23930  dvmptdiv  23950  lhop2  23991  deg1sublt  24083  ig1pval3  24147  dvply1  24252  plydiveu  24266  quotcan  24277  aaliou3lem9  24318  taylthlem2  24341  pserdvlem2  24395  abelthlem9  24407  logccne0  24538  logtayllem  24618  logtayl  24619  cxpef  24624  angrtmuld  24751  isosctrlem2  24762  isosctrlem3  24763  chordthmlem  24772  leibpilem2  24881  leibpi  24882  rlimcnp2  24906  efrlim  24909  vma1  25105  muinv  25132  lgsval2lem  25245  lgsval4  25255  lgsdir  25270  lgseisenlem4  25316  lgsquadlem1  25318  lgsquad2  25324  m1lgs  25326  2sqlem8a  25363  2sqlem8  25364  padicabv  25532  ostth1  25535  ostth3  25540  tgbtwnne  25598  tgbtwndiff  25614  tgcolg  25662  tgbtwnconn1lem3  25682  legso  25707  tglineeltr  25739  tglineintmo  25750  tglineneq  25752  colline  25757  mirne  25775  miriso  25778  mirhl  25787  mirbtwnhl  25788  symquadlem  25797  krippenlem  25798  midexlem  25800  ragncol  25817  footex  25826  colperp  25834  colperpexlem3  25837  mideulem2  25839  opphllem  25840  midex  25842  opptgdim2  25850  oppperpex  25858  hlpasch  25861  colopp  25874  colhp  25875  lmieu  25889  trgcopy  25909  cgracol  25932  cgrg3col4  25947  axlowdimlem15  26049  axcontlem2  26058  axcontlem7  26063  1egrvtxdg0  26634  2pthnloop  26854  cyclnspth  26923  eupth2lem1  27390  eupth2lem2  27391  eupth2lem3lem6  27405  strlem6  29442  hstrlem6  29450  atssma  29564  chirredlem1  29576  znsqcld  29838  xaddeq0  29844  xlt2addrd  29849  divnumden2  29890  2sqcoprm  29971  2sqmod  29972  submomnd  30034  ornglmullt  30131  orngrmullt  30132  ofldchr  30138  suborng  30139  pmtridf1o  30180  pmtridfv1  30181  pmtridfv2  30182  1smat1  30194  submatminr1  30200  madjusmdetlem2  30218  xrge0iifcnv  30303  xrge0iifcv  30304  xrge0iif1  30308  qqhval2lem  30349  qqhf  30354  qqhre  30388  esumrnmpt2  30454  esumcvgre  30477  inelpisys  30541  carsgclctunlem2  30705  ballotlemirc  30917  sgnmul  30928  sgn0bi  30933  signswlid  30960  repr0  31013  reprlt  31021  reprgt  31023  reprinfz1  31024  tgoldbachgtda  31063  tgoldbachgt  31065  bnj1523  31460  fz0n  31936  dfrdg2  32019  nolesgn2ores  32144  nosep1o  32151  nosepdmlem  32152  nosepssdm  32155  noresle  32165  nosupbnd1lem3  32175  nosupbnd1lem4  32176  nosupbnd1lem5  32177  nosupbnd1lem6  32178  nosupbnd2lem1  32180  dfrdg4  32377  broutsideof2  32548  outsidele  32558  rankeq1o  32597  ivthALT  32649  limsucncmpi  32759  topdifinffinlem  33509  icorempt2  33513  finxpreclem2  33541  finxp1o  33543  finxpreclem6  33547  poimirlem9  33729  poimirlem11  33731  poimirlem12  33732  poimirlem25  33745  fdc  33850  heibor1lem  33917  heiborlem4  33922  heiborlem6  33924  2atm  35305  lhpocnle  35794  lhp2at0nle  35813  trlval3  35965  cdleme18c  36071  cdlemg17b  36440  cdlemg17i  36447  dia2dimlem2  36843  dia2dimlem3  36844  dihord6apre  37034  dihatlat  37112  dochshpsat  37232  lcfrlem9  37328  mapdhval2  37504  hdmap1val2  37578  hdmap14lem4a  37649  hdmap14lem6  37651  jm2.26lem3  38066  kelac1  38131  clsk3nimkb  38835  clsk1indlem0  38836  sineq0ALT  39664  refsum2cnlem1  39687  disjxp1  39728  nelrnmpt  39747  disjf1  39855  disjrnmpt2  39861  disjinfi  39866  rnmptn0  39897  oddfl  39968  xrlttri5d  39974  supxrge  40031  nepnfltpnf  40035  nemnftgtmnft  40037  xrlexaddrp  40045  xrred  40058  supminfxr2  40175  icoiccdif  40228  qinioo  40239  ioonct  40241  fmul01lt1lem1  40293  climrec  40312  limcperiod  40337  reclimc  40362  limsupub  40413  cncfiooicclem1  40583  cncfioobdlem  40586  fperdvper  40610  dvdivbd  40615  ditgeqiooicc  40652  itgsincmulx  40666  itgioocnicc  40669  iblcncfioo  40670  stoweidlem35  40728  stoweidlem39  40732  stirlinglem5  40771  stirlinglem8  40774  dirkerper  40789  dirkercncflem2  40797  dirkercncflem4  40799  fourierdlem31  40831  fourierdlem34  40834  fourierdlem41  40841  fourierdlem42  40842  fourierdlem44  40844  fourierdlem48  40847  fourierdlem49  40848  fourierdlem53  40852  fourierdlem56  40855  fourierdlem58  40857  fourierdlem60  40859  fourierdlem61  40860  fourierdlem62  40861  fourierdlem65  40864  fourierdlem66  40865  fourierdlem73  40872  fourierdlem76  40875  fourierdlem79  40878  fourierdlem81  40880  fourierdlem82  40881  fourierdlem93  40892  fourierdlem103  40902  fourierdlem104  40903  sqwvfoura  40921  fourierswlem  40923  elaa2lem  40926  elaa2  40927  etransclem4  40931  etransclem24  40951  etransclem31  40958  etransclem32  40959  etransclem35  40962  sge0repnf  41079  sge0fodjrnlem  41109  sge0iunmpt  41111  sge0rpcpnf  41114  nnfoctbdjlem  41148  meadjun  41155  voliunsge0lem  41165  hoicvr  41241  ovnn0val  41244  ovnsubaddlem1  41263  hoidmvn0val  41277  hsphoidmvle  41279  hoidmv1lelem1  41284  hoidmv1lelem2  41285  hoidmv1lelem3  41286  ovnhoilem1  41294  ovnsubadd2lem  41338  ovnovollem3  41351  lighneallem3  42096  divgcdoddALTV  42165  dignn0flhalflem1  42974
  Copyright terms: Public domain W3C validator