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

Theorem neneqd 2945
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 2941 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2sylib 221 1 (𝜑 → ¬ 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1543  wne 2940
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 2941
This theorem is referenced by:  neneq  2946  necon2bi  2971  necon2i  2975  necon4i  2976  pm2.21ddne  3026  mteqand  3045  nelrdva  3623  eldifsnneq  4709  disjprg  5054  0inp0  5255  rnmptn0  6112  onnseq  8086  sniffsupp  9021  dfac2b  9749  ackbij1lem15  9853  ttukeylem7  10134  fpwwe2lem12  10261  canthnumlem  10267  canthp1lem2  10272  recgt0  11683  nnneneg  11870  elnnz  12191  xrnemnf  12714  xrnepnf  12715  fzprval  13178  fzodisjsn  13285  expnnval  13643  znsqcld  13737  hashelne0d  13940  elprchashprn2  13968  relexpsucnnr  14593  relexp1g  14594  relexpuzrel  14620  sgnp  14658  fprodn0f  15558  ruclem12  15807  dvdsle  15876  nndvdslegcd  16069  gcdnncl  16071  divgcdnn  16079  sqgcd  16127  eucalgf  16145  eucalginv  16146  lcmgcdlem  16168  lcmftp  16198  lcmfunsnlem2lem1  16200  lcmfunsnlem2lem2  16201  qredeu  16220  rpdvds  16222  cncongr2  16230  divnumden  16309  divdenle  16310  phisum  16348  oddprm  16368  pythagtriplem4  16377  pythagtriplem8  16381  pythagtriplem9  16382  4sqlem10  16505  ram0  16580  cat1lem  17607  isipodrs  18048  gsumval2  18163  smndex1n0mnd  18344  smndex2dnrinv  18347  mulgnn  18501  sylow1lem1  18992  gsumval3eu  19294  ablsimpgfindlem1  19499  ablsimpgfindlem2  19500  ablsimpgfind  19502  fincygsubgodd  19504  abvtrivd  19881  00lss  19983  lvecvscan2  20154  fidomndrng  20350  prmirredlem  20464  uvcff  20758  mvrcl  20982  mplmon  20997  mplmonmul  20998  coe1tmfv2  21201  cply1coe0  21225  cply1coe0bi  21226  1marepvsma1  21485  mdetrsca2  21506  mdetrlin2  21509  mdetunilem2  21515  mdetunilem5  21518  mdetunilem6  21519  mdetunilem9  21522  maducoeval2  21542  gsummatr01lem3  21559  gsummatr01lem4  21560  gsummatr01  21561  m2cpm  21643  m2cpminvid2lem  21656  fvmptnn04ifa  21752  fvmptnn04ifb  21753  fvmptnn04ifc  21754  chfacffsupp  21758  chfacfscmul0  21760  chfacfscmulgsum  21762  chfacfpmmul0  21764  chfacfpmmulgsum  21766  connclo  22317  dissnlocfin  22431  ptpjpre2  22482  txindis  22536  snfil  22766  alexsublem  22946  tsmsfbas  23030  stdbdxmet  23418  dscmet  23475  xrsxmet  23711  iccpnfcnv  23846  cphsubrglem  24079  minveclem3b  24330  minveclem4a  24332  ovolicc1  24418  dvexp2  24856  dvmptdiv  24876  lhop2  24917  deg1sublt  25013  ig1pval3  25077  dvply1  25182  plydiveu  25196  quotcan  25207  aaliou3lem9  25248  taylthlem2  25271  pserdvlem2  25325  abelthlem9  25337  logccne0  25472  logtayllem  25552  logtayl  25553  cxpef  25558  angrtmuld  25696  isosctrlem3  25708  chordthmlem  25720  leibpilem2  25829  leibpi  25830  rlimcnp2  25854  efrlim  25857  vma1  26053  muinv  26080  lgsval2lem  26193  lgsval4  26203  lgsdir  26218  lgseisenlem4  26264  lgsquadlem1  26266  lgsquad2  26272  m1lgs  26274  2sqlem8a  26311  2sqlem8  26312  2sqcoprm  26321  2sqmod  26322  padicabv  26516  ostth1  26519  ostth3  26524  tgbtwnne  26586  tgbtwndiff  26602  tgcolg  26650  tgbtwnconn1lem3  26670  legso  26695  tglineeltr  26727  tglineintmo  26738  tglineneq  26740  colline  26745  mirne  26763  miriso  26766  mirhl  26775  mirbtwnhl  26776  symquadlem  26785  krippenlem  26786  midexlem  26788  ragncol  26805  footexALT  26814  footexlem2  26816  colperp  26825  colperpexlem3  26828  mideulem2  26830  opphllem  26831  midex  26833  opptgdim2  26841  oppperpex  26849  hlpasch  26852  colopp  26865  lmieu  26880  trgcopy  26900  cgracol  26924  cgrg3col4  26949  axlowdimlem15  27052  axcontlem2  27061  axcontlem7  27066  1egrvtxdg0  27604  2pthnloop  27823  cyclnspth  27892  eupth2lem1  28306  eupth2lem2  28307  eupth2lem3lem6  28321  strlem6  30342  hstrlem6  30350  atssma  30464  chirredlem1  30476  snsssng  30584  xaddeq0  30801  xlt2addrd  30806  fzone1  30846  divnumden2  30857  submomnd  31060  pmtridf1o  31085  pmtridfv1  31086  pmtridfv2  31087  ornglmullt  31230  orngrmullt  31231  ofldchr  31237  suborng  31238  pidlnz  31290  lindssn  31292  0ringprmidl  31344  qsidomlem1  31347  mxidlprm  31359  krull  31362  lindsunlem  31424  1smat1  31473  submatminr1  31479  madjusmdetlem2  31497  zarcls1  31538  zarclsint  31541  zarclssn  31542  xrge0iifcnv  31602  xrge0iifcv  31603  xrge0iif1  31607  qqhval2lem  31648  qqhf  31653  qqhre  31687  esumrnmpt2  31753  esumcvgre  31776  inelpisys  31839  carsgclctunlem2  32003  ballotlemirc  32215  sgnmul  32226  sgn0bi  32231  signswlid  32255  repr0  32308  reprlt  32316  reprgt  32318  reprinfz1  32319  tgoldbachgtda  32358  tgoldbachgt  32360  bnj1523  32769  acycgr2v  32830  fmlaomn0  33070  fmlasucdisj  33079  fz0n  33419  dfrdg2  33495  frxp2  33533  frxp3  33539  nolesgn2ores  33617  nogesgn1ores  33619  nosep1o  33626  nosep2o  33627  nosepdmlem  33628  nosepssdm  33631  noresle  33642  nosupbnd1lem3  33655  nosupbnd1lem4  33656  nosupbnd1lem5  33657  nosupbnd1lem6  33658  nosupbnd2lem1  33660  noinfbnd1lem3  33670  noinfbnd1lem4  33671  noinfbnd1lem5  33672  noinfbnd1lem6  33673  noinfbnd2lem1  33675  dfrdg4  33995  broutsideof2  34166  outsidele  34176  rankeq1o  34215  ivthALT  34266  limsucncmpi  34376  topdifinffinlem  35260  icorempo  35264  finxpreclem2  35303  finxp1o  35305  finxpreclem6  35309  poimirlem9  35528  poimirlem11  35530  poimirlem12  35531  poimirlem25  35544  fdc  35645  heibor1lem  35709  heiborlem4  35714  heiborlem6  35716  2atm  37283  lhpocnle  37772  lhp2at0nle  37791  trlval3  37943  cdleme18c  38049  cdlemg17b  38418  cdlemg17i  38425  dia2dimlem2  38821  dia2dimlem3  38822  dihord6apre  39012  dihatlat  39090  dochshpsat  39210  lcfrlem9  39306  mapdhval2  39482  hdmap1val2  39556  hdmap14lem4a  39627  hdmap14lem6  39629  dvrelogpow2b  39814  aks4d1p1p4  39817  aks4d1p6  39827  sticksstones1  39832  sticksstones10  39841  sticksstones12a  39843  sticksstones12  39844  sticksstones22  39854  metakunt6  39860  metakunt7  39861  metakunt11  39865  metakunt12  39866  metakunt27  39881  metakunt28  39882  metakunt29  39883  metakunt30  39884  mhpind  40001  negn0nposznnd  40025  nn0rppwr  40049  rtprmirr  40063  prjspner1  40179  dffltz  40182  3cubeslem2  40218  jm2.26lem3  40534  kelac1  40599  clsk1indlem0  41336  finnzfsuppd  41506  scotteld  41545  sineq0ALT  42238  refsum2cnlem1  42261  disjxp1  42298  nelrnmpt  42315  disjf1  42401  disjrnmpt2  42407  disjinfi  42412  oddfl  42496  xrlttri5d  42502  supxrge  42558  nepnfltpnf  42562  nemnftgtmnft  42564  xrlexaddrp  42572  xrred  42585  supminfxr2  42692  icoiccdif  42745  qinioo  42756  ioonct  42758  fmul01lt1lem1  42808  climrec  42827  limcperiod  42852  reclimc  42877  limsupub  42928  liminflbuz2  43039  cncfiooicclem1  43117  cncfioobdlem  43120  fperdvper  43143  dvdivbd  43147  ditgeqiooicc  43184  itgsincmulx  43198  itgioocnicc  43201  iblcncfioo  43202  stoweidlem35  43259  stoweidlem39  43263  stirlinglem5  43302  stirlinglem8  43305  dirkerper  43320  dirkercncflem2  43328  dirkercncflem4  43330  fourierdlem31  43362  fourierdlem34  43365  fourierdlem41  43372  fourierdlem42  43373  fourierdlem44  43375  fourierdlem48  43378  fourierdlem49  43379  fourierdlem53  43383  fourierdlem56  43386  fourierdlem58  43388  fourierdlem60  43390  fourierdlem61  43391  fourierdlem62  43392  fourierdlem65  43395  fourierdlem66  43396  fourierdlem73  43403  fourierdlem76  43406  fourierdlem79  43409  fourierdlem81  43411  fourierdlem82  43412  fourierdlem93  43423  fourierdlem103  43433  fourierdlem104  43434  sqwvfoura  43452  fourierswlem  43454  elaa2lem  43457  elaa2  43458  etransclem4  43462  etransclem24  43482  etransclem31  43489  etransclem32  43490  etransclem35  43493  sge0repnf  43607  sge0fodjrnlem  43637  sge0iunmpt  43639  sge0rpcpnf  43642  nnfoctbdjlem  43676  meadjun  43683  voliunsge0lem  43693  hoicvr  43769  ovnn0val  43772  ovnsubaddlem1  43791  hoidmvn0val  43805  hsphoidmvle  43807  hoidmv1lelem1  43812  hoidmv1lelem2  43813  hoidmv1lelem3  43814  ovnhoilem1  43822  ovnsubadd2lem  43866  ovnovollem3  43879  lighneallem3  44740  divgcdoddALTV  44815  dignn0flhalflem1  45642  itcoval2  45691  itcoval3  45692  itcovalsuc  45694  ackvalsuc1mpt  45705  line2xlem  45780
  Copyright terms: Public domain W3C validator