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

Theorem neneqd 3016
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 3012 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2sylib 221 1 (𝜑 → ¬ 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1538  wne 3011
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 3012
This theorem is referenced by:  neneq  3017  necon2bi  3041  necon2i  3045  necon4i  3046  pm2.21ddne  3095  mteqand  3114  nelrdva  3671  eldifsnneq  4697  disjprg  5038  0inp0  5236  onnseq  7968  sniffsupp  8861  dfac2b  9545  ackbij1lem15  9645  ttukeylem7  9926  fpwwe2lem13  10053  canthnumlem  10059  canthp1lem2  10064  recgt0  11475  nnneneg  11660  elnnz  11979  xrnemnf  12500  xrnepnf  12501  fzprval  12963  fzodisjsn  13070  expnnval  13428  znsqcld  13522  hashelne0d  13725  elprchashprn2  13753  relexpsucnnr  14375  relexp1g  14376  relexpuzrel  14402  sgnp  14440  fprodn0f  15336  ruclem12  15585  dvdsle  15651  nndvdslegcd  15843  gcdnncl  15845  divgcdnn  15852  sqgcd  15898  eucalgf  15916  eucalginv  15917  lcmgcdlem  15939  lcmftp  15969  lcmfunsnlem2lem1  15971  lcmfunsnlem2lem2  15972  qredeu  15991  rpdvds  15993  cncongr2  16001  divnumden  16077  divdenle  16078  phisum  16116  oddprm  16136  pythagtriplem4  16145  pythagtriplem8  16149  pythagtriplem9  16150  4sqlem10  16272  ram0  16347  isipodrs  17762  gsumval2  17887  smndex1n0mnd  18068  smndex2dnrinv  18071  mulgnn  18223  sylow1lem1  18714  gsumval3eu  19015  ablsimpgfindlem1  19220  ablsimpgfindlem2  19221  ablsimpgfind  19223  fincygsubgodd  19225  abvtrivd  19602  00lss  19704  lvecvscan2  19875  fidomndrng  20071  prmirredlem  20184  uvcff  20478  mvrcl  20686  mplmon  20701  mplmonmul  20702  coe1tmfv2  20902  cply1coe0  20926  cply1coe0bi  20927  1marepvsma1  21186  mdetrsca2  21207  mdetrlin2  21210  mdetunilem2  21216  mdetunilem5  21219  mdetunilem6  21220  mdetunilem9  21223  maducoeval2  21243  gsummatr01lem3  21260  gsummatr01lem4  21261  gsummatr01  21262  m2cpm  21344  m2cpminvid2lem  21357  fvmptnn04ifa  21453  fvmptnn04ifb  21454  fvmptnn04ifc  21455  chfacffsupp  21459  chfacfscmul0  21461  chfacfscmulgsum  21463  chfacfpmmul0  21465  chfacfpmmulgsum  21467  connclo  22018  dissnlocfin  22132  ptpjpre2  22183  txindis  22237  snfil  22467  alexsublem  22647  tsmsfbas  22731  stdbdxmet  23120  dscmet  23177  xrsxmet  23412  iccpnfcnv  23547  cphsubrglem  23780  minveclem3b  24030  minveclem4a  24032  ovolicc1  24118  dvexp2  24555  dvmptdiv  24575  lhop2  24616  deg1sublt  24709  ig1pval3  24773  dvply1  24878  plydiveu  24892  quotcan  24903  aaliou3lem9  24944  taylthlem2  24967  pserdvlem2  25021  abelthlem9  25033  logccne0  25168  logtayllem  25248  logtayl  25249  cxpef  25254  angrtmuld  25392  isosctrlem3  25404  chordthmlem  25416  leibpilem2  25525  leibpi  25526  rlimcnp2  25550  efrlim  25553  vma1  25749  muinv  25776  lgsval2lem  25889  lgsval4  25899  lgsdir  25914  lgseisenlem4  25960  lgsquadlem1  25962  lgsquad2  25968  m1lgs  25970  2sqlem8a  26007  2sqlem8  26008  2sqcoprm  26017  2sqmod  26018  padicabv  26212  ostth1  26215  ostth3  26220  tgbtwnne  26282  tgbtwndiff  26298  tgcolg  26346  tgbtwnconn1lem3  26366  legso  26391  tglineeltr  26423  tglineintmo  26434  tglineneq  26436  colline  26441  mirne  26459  miriso  26462  mirhl  26471  mirbtwnhl  26472  symquadlem  26481  krippenlem  26482  midexlem  26484  ragncol  26501  footexALT  26510  footexlem2  26512  colperp  26521  colperpexlem3  26524  mideulem2  26526  opphllem  26527  midex  26529  opptgdim2  26537  oppperpex  26545  hlpasch  26548  colopp  26561  lmieu  26576  trgcopy  26596  cgracol  26620  cgrg3col4  26645  axlowdimlem15  26748  axcontlem2  26757  axcontlem7  26762  1egrvtxdg0  27299  2pthnloop  27518  cyclnspth  27587  eupth2lem1  28001  eupth2lem2  28002  eupth2lem3lem6  28016  strlem6  30037  hstrlem6  30045  atssma  30159  chirredlem1  30171  snsssng  30282  xaddeq0  30487  xlt2addrd  30492  fzone1  30533  divnumden2  30544  submomnd  30742  pmtridf1o  30767  pmtridfv1  30768  pmtridfv2  30769  ornglmullt  30912  orngrmullt  30913  ofldchr  30919  suborng  30920  pidlnz  30972  lindssn  30974  qsidomlem1  31007  mxidlprm  31019  krull  31022  lindsunlem  31077  1smat1  31126  submatminr1  31132  madjusmdetlem2  31150  zarcls1  31191  zarclsint  31194  zarclssn  31195  xrge0iifcnv  31250  xrge0iifcv  31251  xrge0iif1  31255  qqhval2lem  31296  qqhf  31301  qqhre  31335  esumrnmpt2  31401  esumcvgre  31424  inelpisys  31487  carsgclctunlem2  31651  ballotlemirc  31863  sgnmul  31874  sgn0bi  31879  signswlid  31903  repr0  31956  reprlt  31964  reprgt  31966  reprinfz1  31967  tgoldbachgtda  32006  tgoldbachgt  32008  bnj1523  32417  acycgr2v  32471  fmlaomn0  32711  fmlasucdisj  32720  fz0n  33036  dfrdg2  33114  nolesgn2ores  33253  nosep1o  33260  nosepdmlem  33261  nosepssdm  33264  noresle  33274  nosupbnd1lem3  33284  nosupbnd1lem4  33285  nosupbnd1lem5  33286  nosupbnd1lem6  33287  nosupbnd2lem1  33289  dfrdg4  33486  broutsideof2  33657  outsidele  33667  rankeq1o  33706  ivthALT  33757  limsucncmpi  33867  topdifinffinlem  34725  icorempo  34729  finxpreclem2  34768  finxp1o  34770  finxpreclem6  34774  poimirlem9  35025  poimirlem11  35027  poimirlem12  35028  poimirlem25  35041  fdc  35142  heibor1lem  35206  heiborlem4  35211  heiborlem6  35213  2atm  36782  lhpocnle  37271  lhp2at0nle  37290  trlval3  37442  cdleme18c  37548  cdlemg17b  37917  cdlemg17i  37924  dia2dimlem2  38320  dia2dimlem3  38321  dihord6apre  38511  dihatlat  38589  dochshpsat  38709  lcfrlem9  38805  mapdhval2  38981  hdmap1val2  39055  hdmap14lem4a  39126  hdmap14lem6  39128  metakunt6  39315  metakunt7  39316  metakunt11  39320  metakunt12  39321  negn0nposznnd  39421  nn0rppwr  39435  rtprmirr  39447  dffltz  39546  3cubeslem2  39557  jm2.26lem3  39873  kelac1  39938  clsk1indlem0  40678  finnzfsuppd  40850  scotteld  40889  sineq0ALT  41578  refsum2cnlem1  41601  disjxp1  41638  nelrnmpt  41655  disjf1  41748  disjrnmpt2  41754  disjinfi  41759  rnmptn0  41789  oddfl  41848  xrlttri5d  41854  supxrge  41910  nepnfltpnf  41914  nemnftgtmnft  41916  xrlexaddrp  41924  xrred  41937  supminfxr2  42048  icoiccdif  42101  qinioo  42112  ioonct  42114  fmul01lt1lem1  42166  climrec  42185  limcperiod  42210  reclimc  42235  limsupub  42286  liminflbuz2  42397  cncfiooicclem1  42475  cncfioobdlem  42478  fperdvper  42501  dvdivbd  42505  ditgeqiooicc  42542  itgsincmulx  42556  itgioocnicc  42559  iblcncfioo  42560  stoweidlem35  42617  stoweidlem39  42621  stirlinglem5  42660  stirlinglem8  42663  dirkerper  42678  dirkercncflem2  42686  dirkercncflem4  42688  fourierdlem31  42720  fourierdlem34  42723  fourierdlem41  42730  fourierdlem42  42731  fourierdlem44  42733  fourierdlem48  42736  fourierdlem49  42737  fourierdlem53  42741  fourierdlem56  42744  fourierdlem58  42746  fourierdlem60  42748  fourierdlem61  42749  fourierdlem62  42750  fourierdlem65  42753  fourierdlem66  42754  fourierdlem73  42761  fourierdlem76  42764  fourierdlem79  42767  fourierdlem81  42769  fourierdlem82  42770  fourierdlem93  42781  fourierdlem103  42791  fourierdlem104  42792  sqwvfoura  42810  fourierswlem  42812  elaa2lem  42815  elaa2  42816  etransclem4  42820  etransclem24  42840  etransclem31  42847  etransclem32  42848  etransclem35  42851  sge0repnf  42965  sge0fodjrnlem  42995  sge0iunmpt  42997  sge0rpcpnf  43000  nnfoctbdjlem  43034  meadjun  43041  voliunsge0lem  43051  hoicvr  43127  ovnn0val  43130  ovnsubaddlem1  43149  hoidmvn0val  43163  hsphoidmvle  43165  hoidmv1lelem1  43170  hoidmv1lelem2  43171  hoidmv1lelem3  43172  ovnhoilem1  43180  ovnsubadd2lem  43224  ovnovollem3  43237  lighneallem3  44065  divgcdoddALTV  44140  dignn0flhalflem1  44969  itcoval2  45018  itcoval3  45019  itcovalsuc  45021  ackvalsuc1mpt  45032  line2xlem  45107
  Copyright terms: Public domain W3C validator