MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.61dane Unicode version

Theorem pm2.61dane 2775
Description: Deduction eliminating an inequality in an antecedent. (Contributed by NM, 30-Nov-2011.)
Hypotheses
Ref Expression
pm2.61dane.1
pm2.61dane.2
Assertion
Ref Expression
pm2.61dane

Proof of Theorem pm2.61dane
StepHypRef Expression
1 pm2.61dane.1 . . 3
21ex 434 . 2
3 pm2.61dane.2 . . 3
43ex 434 . 2
52, 4pm2.61dne 2774 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  =/=wne 2652
This theorem is referenced by:  pm2.61da2ne  2776  pm2.61da3ne  2777  pm2.61da3neOLD  2778  pm2.61iine  2779  disjxiun  4449  onfr  4922  f1oprswap  5860  soex  6743  riiner  7403  difsnen  7619  mapdom2  7708  nnunifi  7791  fofinf1o  7821  brwdom2  8020  cantnff  8114  cantnfp1  8121  cantnfp1OLD  8147  carddomi2  8372  wdomfil  8463  fin1a2lem10  8810  fin1a2lem11  8811  uzsupss  11203  xaddcom  11466  xnegdi  11469  xpncan  11472  xleadd1a  11474  xsubge0  11482  cnpart  13073  fsumcllem  13554  fsumrev2  13597  expcnv  13675  geomulcvg  13685  fprodcllem  13758  fsumdvds  14029  gcd0id  14161  nn0seqcvgd  14199  mulgcddvds  14245  pcge0  14385  pcneg  14397  pcdvdstr  14399  pcz  14404  pcprmpw2  14405  pcadd  14408  ramcl2  14534  0ramcl  14541  ramub1lem1  14544  ramcl  14547  mrerintcl  14994  mreriincl  14995  mreexexlem4d  15044  mreclatBAD  15817  psgnunilem1  16518  odmulg  16578  sylow1lem1  16618  pgpfi  16625  odadd1  16854  odadd2  16855  gsumval3OLD  16908  gsumval3  16911  gsumpt  16988  gsumptOLD  16989  dprdfcntz  17049  dprdfcntzOLD  17055  dprd2da  17091  ablfac1eulem  17123  pgpfaclem3  17134  abvneg  17483  lssssr  17599  lspsneq  17768  lspdisj2  17773  drngnidl  17877  cnsubrg  18478  riinopn  19417  riincld  19545  neipeltop  19630  hauscmplem  19906  cmpfi  19908  ptbasfi  20082  xkoccn  20120  txindislem  20134  txtube  20141  hmphindis  20298  fclscmp  20531  utop2nei  20753  nrginvrcn  21200  nmoleub  21238  blcvx  21303  xrsxmet  21314  xrsblre  21316  lebnumlem3  21463  cphsqrtcl2  21633  ovollb2  21900  ioorcl  21986  i1fmulc  22110  itg1mulc  22111  mbfi1fseqlem4  22125  dvlip  22394  dvne0  22412  ig1pdvds  22577  plyeq0lem  22607  plyeq0  22608  aannenlem2  22725  aalioulem6  22733  abelthlem8  22834  abelth  22836  cxpexp  23049  cxpge0  23064  cxpmul2  23070  abscxp2  23074  abscxpbnd  23127  cxpeq  23131  isosctrlem2  23153  atanrecl  23242  wilthlem2  23343  dchrabs2  23537  dchr1re  23538  lgsneg1  23595  lgsdirprm  23604  lgsdir  23605  lgsne0  23608  lgsdirnn0  23614  lgsdinn0  23615  2sqlem9  23648  rpvmasumlem  23672  dchrvmasumiflem1  23686  dchrisum0flblem1  23693  rpvmasum2  23697  pntrsumbnd2  23752  pntleml  23796  tgcgrextend  23876  tgbtwnexch2  23887  tgifscgr  23900  tgcolg  23941  tgidinside  23958  tgbtwnconn1lem2  23960  tgbtwnconn1lem3  23961  tglinethru  24016  tglnpt2  24021  tglineneq  24024  coltr  24027  coltr3  24029  colline  24030  mirreu3  24035  miriso  24050  mirln  24056  mirln2  24057  mirconn  24058  mirbtwnhl  24060  colmid  24065  krippenlem  24067  midexlem  24069  ragflat  24081  ragcgr  24084  perprag  24100  perpdragALT  24101  colperpexlem1  24104  colperpexlem3  24106  midex  24111  opphllem1  24119  opphllem2  24120  opphllem5  24123  opphllem6  24124  lmiisolem  24161  hypcgrlem1  24164  hypcgrlem2  24165  umgraex  24323  eupath2lem3  24979  nmcoplbi  26947  nmophmi  26950  nmbdfnlbi  26968  disjdifprg  27436  imadifxp  27458  xlt2addrd  27578  ssnnssfz  27597  locfinref  27844  nnlogbexp  28020  esumpr2  28074  mbfmcst  28230  probun  28358  0rrv  28390  sgncl  28477  signsvtn0  28527  signstfvneq0  28529  btwnconn1lem11  29747  mblfinlem1  30051  mblfinlem2  30052  ismblfin  30055  itg2addnclem  30066  itgaddnclem2  30074  bddiblnc  30085  areacirclem4  30110  areacirc  30112  isbnd3  30280  blbnd  30283  rrnequiv  30331  jm2.19  30935  jm2.23  30938  lcmdvds  31214  nzss  31222  stoweidlem58  31840  fourierdlem41  31930  fourierdlem48  31937  fouriersw  32014  etransclem24  32041  ssnn0ssfz  32938  lsmsat  34733  lkrscss  34823  eqlkr  34824  lkrshpor  34832  atcvrj2b  35156  atltcvr  35159  3dim1  35191  3dim2  35192  3dim3  35193  ps-2  35202  2at0mat0  35249  dalemdnee  35390  dalem63  35459  lnatexN  35503  2llnma3r  35512  pmodlem1  35570  pmapjat1  35577  pclfinclN  35674  osumclN  35691  pexmidALTN  35702  lhpexle2lem  35733  lhpexle3lem  35735  4atexlemex6  35798  4atex  35800  trlnle  35911  trlval3  35912  cdlemc  35922  cdlemd9  35931  cdleme27N  36095  cdleme28c  36098  cdleme32fvaw  36165  cdleme42ke  36211  cdleme42keg  36212  cdleme42mgN  36214  cdleme17d  36224  cdleme48fvg  36226  cdleme50trn123  36280  cdlemb3  36332  cdlemg8  36357  cdlemg15a  36381  cdlemg15  36382  cdlemg16  36383  cdlemg16ALTN  36384  cdlemg16z  36385  cdlemg16zz  36386  cdlemg20  36411  cdlemg22  36413  cdlemg37  36415  cdlemg31d  36426  cdlemg39  36442  cdlemg40  36443  ltrncom  36464  tendotr  36556  cdlemk25-3  36630  cdlemk35s-id  36664  cdlemk39s-id  36666  cdlemk53b  36682  cdlemk53  36683  cdlemk55  36687  cdlemk35u  36690  cdlemk55u  36692  cdlemk39u  36694  cdlemk19u  36696  cdleml5N  36706  dia2dimlem7  36797  dia2dimlem13  36803  dih1dimatlem  37056  dihlsprn  37058  dihjat1lem  37155  dihjat1  37156  dvh2dim  37172  dochexmid  37195  lclkrlem1  37233  lclkrlem2i  37242  lclkrlem2t  37253  lcfrlem34  37303  lcfrlem38  37307  lcfrlem41  37310  mapdindp1  37447  mapdindp2  37448  mapdh6dN  37466  mapdh6jN  37472  mapdh8j  37515  mapdh8  37516  hdmap1l6d  37541  hdmap1l6j  37547  hdmap11lem2  37572  hdmap14lem7  37604
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 185  df-an 371  df-ne 2654
  Copyright terms: Public domain W3C validator