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

Theorem neneqd 3021
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 3017 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2sylib 219 1 (𝜑 → ¬ 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  wne 3016
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 208  df-ne 3017
This theorem is referenced by:  neneq  3022  necon2bi  3046  necon2i  3050  necon4i  3051  pm2.21ddne  3101  mteqand  3122  nelrdva  3695  eldifsnneq  4717  disjprg  5054  0inp0  5251  onnseq  7972  sniffsupp  8862  dfac2b  9545  ackbij1lem15  9645  ttukeylem7  9926  fpwwe2lem13  10053  canthnumlem  10059  canthp1lem2  10064  recgt0  11475  nnneneg  11661  elnnz  11980  xrnemnf  12502  xrnepnf  12503  fzprval  12958  fzodisjsn  13065  expnnval  13422  znsqcld  13516  hashelne0d  13719  elprchashprn2  13747  relexpsucnnr  14374  relexp1g  14375  relexpuzrel  14401  sgnp  14439  fprodn0f  15335  ruclem12  15584  dvdsle  15650  nndvdslegcd  15844  gcdnncl  15846  divgcdnn  15853  sqgcd  15899  eucalgf  15917  eucalginv  15918  lcmgcdlem  15940  lcmftp  15970  lcmfunsnlem2lem1  15972  lcmfunsnlem2lem2  15973  qredeu  15992  rpdvds  15994  cncongr2  16002  divnumden  16078  divdenle  16079  phisum  16117  oddprm  16137  pythagtriplem4  16146  pythagtriplem8  16150  pythagtriplem9  16151  4sqlem10  16273  ram0  16348  isipodrs  17761  gsumval2  17886  mulgnn  18172  sylow1lem1  18654  gsumval3eu  18955  ablsimpgfindlem1  19160  ablsimpgfindlem2  19161  ablsimpgfind  19163  fincygsubgodd  19165  abvtrivd  19542  00lss  19644  lvecvscan2  19815  fidomndrng  20010  mvrcl  20159  mplmon  20174  mplmonmul  20175  coe1tmfv2  20373  cply1coe0  20397  cply1coe0bi  20398  prmirredlem  20570  uvcff  20865  1marepvsma1  21122  mdetrsca2  21143  mdetrlin2  21146  mdetunilem2  21152  mdetunilem5  21155  mdetunilem6  21156  mdetunilem9  21159  maducoeval2  21179  gsummatr01lem3  21196  gsummatr01lem4  21197  gsummatr01  21198  m2cpm  21279  m2cpminvid2lem  21292  fvmptnn04ifa  21388  fvmptnn04ifb  21389  fvmptnn04ifc  21390  chfacffsupp  21394  chfacfscmul0  21396  chfacfscmulgsum  21398  chfacfpmmul0  21400  chfacfpmmulgsum  21402  connclo  21953  dissnlocfin  22067  ptpjpre2  22118  txindis  22172  snfil  22402  alexsublem  22582  tsmsfbas  22665  stdbdxmet  23054  dscmet  23111  xrsxmet  23346  iccpnfcnv  23477  cphsubrglem  23710  minveclem3b  23960  minveclem4a  23962  ovolicc1  24046  dvexp2  24480  dvmptdiv  24500  lhop2  24541  deg1sublt  24633  ig1pval3  24697  dvply1  24802  plydiveu  24816  quotcan  24827  aaliou3lem9  24868  taylthlem2  24891  pserdvlem2  24945  abelthlem9  24957  logccne0  25089  logtayllem  25169  logtayl  25170  cxpef  25175  angrtmuld  25313  isosctrlem3  25325  chordthmlem  25337  leibpilem2  25447  leibpi  25448  rlimcnp2  25472  efrlim  25475  vma1  25671  muinv  25698  lgsval2lem  25811  lgsval4  25821  lgsdir  25836  lgseisenlem4  25882  lgsquadlem1  25884  lgsquad2  25890  m1lgs  25892  2sqlem8a  25929  2sqlem8  25930  2sqcoprm  25939  2sqmod  25940  padicabv  26134  ostth1  26137  ostth3  26142  tgbtwnne  26204  tgbtwndiff  26220  tgcolg  26268  tgbtwnconn1lem3  26288  legso  26313  tglineeltr  26345  tglineintmo  26356  tglineneq  26358  colline  26363  mirne  26381  miriso  26384  mirhl  26393  mirbtwnhl  26394  symquadlem  26403  krippenlem  26404  midexlem  26406  ragncol  26423  footexALT  26432  footexlem2  26434  colperp  26443  colperpexlem3  26446  mideulem2  26448  opphllem  26449  midex  26451  opptgdim2  26459  oppperpex  26467  hlpasch  26470  colopp  26483  lmieu  26498  trgcopy  26518  cgracol  26542  cgrg3col4  26567  axlowdimlem15  26670  axcontlem2  26679  axcontlem7  26684  1egrvtxdg0  27221  2pthnloop  27440  cyclnspth  27509  eupth2lem1  27925  eupth2lem2  27926  eupth2lem3lem6  27940  strlem6  29961  hstrlem6  29969  atssma  30083  chirredlem1  30095  xaddeq0  30404  xlt2addrd  30409  fzone1  30450  divnumden2  30461  submomnd  30639  pmtridf1o  30664  pmtridfv1  30665  pmtridfv2  30666  ornglmullt  30808  orngrmullt  30809  ofldchr  30815  suborng  30816  lindssn  30867  qsidomlem1  30883  lindsunlem  30920  1smat1  30969  submatminr1  30975  madjusmdetlem2  30993  xrge0iifcnv  31076  xrge0iifcv  31077  xrge0iif1  31081  qqhval2lem  31122  qqhf  31127  qqhre  31161  esumrnmpt2  31227  esumcvgre  31250  inelpisys  31313  carsgclctunlem2  31477  ballotlemirc  31689  sgnmul  31700  sgn0bi  31705  signswlid  31729  repr0  31782  reprlt  31790  reprgt  31792  reprinfz1  31793  tgoldbachgtda  31832  tgoldbachgt  31834  bnj1523  32241  acycgr2v  32295  fmlaomn0  32535  fmlasucdisj  32544  fz0n  32860  dfrdg2  32938  nolesgn2ores  33077  nosep1o  33084  nosepdmlem  33085  nosepssdm  33088  noresle  33098  nosupbnd1lem3  33108  nosupbnd1lem4  33109  nosupbnd1lem5  33110  nosupbnd1lem6  33111  nosupbnd2lem1  33113  dfrdg4  33310  broutsideof2  33481  outsidele  33491  rankeq1o  33530  ivthALT  33581  limsucncmpi  33691  topdifinffinlem  34511  icorempo  34515  finxpreclem2  34554  finxp1o  34556  finxpreclem6  34560  poimirlem9  34783  poimirlem11  34785  poimirlem12  34786  poimirlem25  34799  fdc  34903  heibor1lem  34970  heiborlem4  34975  heiborlem6  34977  2atm  36545  lhpocnle  37034  lhp2at0nle  37053  trlval3  37205  cdleme18c  37311  cdlemg17b  37680  cdlemg17i  37687  dia2dimlem2  38083  dia2dimlem3  38084  dihord6apre  38274  dihatlat  38352  dochshpsat  38472  lcfrlem9  38568  mapdhval2  38744  hdmap1val2  38818  hdmap14lem4a  38889  hdmap14lem6  38891  negn0nposznnd  39048  nn0rppwr  39062  rtprmirr  39074  dffltz  39151  3cubeslem2  39162  jm2.26lem3  39478  kelac1  39543  clsk1indlem0  40271  scotteld  40462  sineq0ALT  41151  refsum2cnlem1  41174  disjxp1  41211  nelrnmpt  41228  disjf1  41323  disjrnmpt2  41329  disjinfi  41334  rnmptn0  41364  oddfl  41423  xrlttri5d  41429  supxrge  41486  nepnfltpnf  41490  nemnftgtmnft  41492  xrlexaddrp  41500  xrred  41513  supminfxr2  41625  icoiccdif  41680  qinioo  41691  ioonct  41693  fmul01lt1lem1  41745  climrec  41764  limcperiod  41789  reclimc  41814  limsupub  41865  liminflbuz2  41976  cncfiooicclem1  42056  cncfioobdlem  42059  fperdvper  42083  dvdivbd  42088  ditgeqiooicc  42125  itgsincmulx  42139  itgioocnicc  42142  iblcncfioo  42143  stoweidlem35  42201  stoweidlem39  42205  stirlinglem5  42244  stirlinglem8  42247  dirkerper  42262  dirkercncflem2  42270  dirkercncflem4  42272  fourierdlem31  42304  fourierdlem34  42307  fourierdlem41  42314  fourierdlem42  42315  fourierdlem44  42317  fourierdlem48  42320  fourierdlem49  42321  fourierdlem53  42325  fourierdlem56  42328  fourierdlem58  42330  fourierdlem60  42332  fourierdlem61  42333  fourierdlem62  42334  fourierdlem65  42337  fourierdlem66  42338  fourierdlem73  42345  fourierdlem76  42348  fourierdlem79  42351  fourierdlem81  42353  fourierdlem82  42354  fourierdlem93  42365  fourierdlem103  42375  fourierdlem104  42376  sqwvfoura  42394  fourierswlem  42396  elaa2lem  42399  elaa2  42400  etransclem4  42404  etransclem24  42424  etransclem31  42431  etransclem32  42432  etransclem35  42435  sge0repnf  42549  sge0fodjrnlem  42579  sge0iunmpt  42581  sge0rpcpnf  42584  nnfoctbdjlem  42618  meadjun  42625  voliunsge0lem  42635  hoicvr  42711  ovnn0val  42714  ovnsubaddlem1  42733  hoidmvn0val  42747  hsphoidmvle  42749  hoidmv1lelem1  42754  hoidmv1lelem2  42755  hoidmv1lelem3  42756  ovnhoilem1  42764  ovnsubadd2lem  42808  ovnovollem3  42821  lighneallem3  43619  divgcdoddALTV  43694  smndex1n0mnd  43982  smndex2dnrinv  43985  dignn0flhalflem1  44573  line2xlem  44638
  Copyright terms: Public domain W3C validator