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

Theorem pm2.61dan 791
Description: Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)
Hypotheses
Ref Expression
pm2.61dan.1
pm2.61dan.2
Assertion
Ref Expression
pm2.61dan

Proof of Theorem pm2.61dan
StepHypRef Expression
1 pm2.61dan.1 . . 3
21ex 434 . 2
3 pm2.61dan.2 . . 3
43ex 434 . 2
52, 4pm2.61d 158 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  /\wa 369
This theorem is referenced by:  pm2.61ddan  792  pm2.61dda  793  nfsb4t  2130  ifeq1da  3971  ifeq2da  3972  ifclda  3973  ifeqda  3974  ifbothda  3976  2if2  3989  posn  5073  frsn  5075  somin1  5408  xpcan  5448  fvmpti  5955  fvmptss  5964  funressn  6084  ovima0  6454  oeoa  7265  oeoe  7267  omabs  7315  eceqoveq  7435  domdifsn  7620  pw2f1olem  7641  mapdom1  7702  marypha1lem  7913  supval2  7935  infdifsn  8094  carden2b  8369  fidomtri  8395  dfac12lem2  8545  cdadom1  8587  infunsdom1  8614  infunsdom  8615  itunisuc  8820  gchdomtri  9028  xrmax2  11406  xrmin1  11407  ifle  11425  xmulneg1  11490  xrsupsslem  11527  xrinfmsslem  11528  fzneuz  11788  seqf1olem1  12146  bccmpl  12387  bcval5  12396  bcpasc  12399  bccl  12400  hasheni  12421  hashfn  12443  hashdom  12447  hashdomi  12448  hashge1  12457  hashbc  12502  sumz  13544  sumss  13546  sumsplit  13583  prod1  13751  prodss  13754  bitsmod  14086  sadadd2lem2  14100  sadcaddlem  14107  gcddvds  14153  gcdcl  14155  gcdneg  14164  pcgcd  14401  pcmpt  14411  pcmpt2  14412  pcprod  14414  fldivp1  14416  prmreclem4  14437  vdwlem6  14504  ramub1lem1  14544  cidpropd  15105  rescabs  15202  lubval  15614  glbval  15627  joinval  15635  meetval  15649  acsexdimd  15813  gsumpropd2lem  15900  gsumval2  15907  f1otrspeq  16472  pmtrfinv  16486  psgnunilem1  16518  gsumval3OLD  16908  gsumval3  16911  ablfac1c  17122  ablfac1eu  17124  mgpress  17152  psrbas  18030  psrbasOLD  18031  resspsrbas  18070  mplmonmul  18126  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  opsrle  18140  opsrbaslem  18142  psrbaspropd  18276  mplbaspropd  18278  frlmsslsp  18829  frlmsslspOLD  18830  mdetdiag  19101  mdetunilem7  19120  mdetunilem9  19122  maducoeval2  19142  madurid  19146  opnnei  19621  restbas  19659  hauspwdom  20002  ptcmplem5  20556  xrsmopn  21317  xrhmeo  21446  lebnum  21464  pcohtpylem  21519  pcoass  21524  pcorevlem  21526  icombl  21974  ioombl  21975  mbfconstlem  22036  mbfima  22039  i1fd  22088  mbfi1fseqlem5  22126  itg2const2  22148  itg2seq  22149  itg2uba  22150  itg2splitlem  22155  itg2split  22156  itg2monolem1  22157  itg2gt0  22167  itg2cnlem1  22168  itg2cnlem2  22169  iblss  22211  iblss2  22212  itgss  22218  bddmulibl  22245  coemullem  22647  aaliou2b  22737  isppw2  23389  mule1  23422  ppip1le  23435  dchrelbas3  23513  dchrpt  23542  bposlem3  23561  bposlem5  23563  bposlem6  23564  lgslem4  23574  lgsneg  23594  lgsmod  23596  lgsdilem  23597  lgsdir  23605  lgsdi  23607  lgsne0  23608  lgsquad3  23636  dchrvmasum2if  23682  midexlem  24069  colperpex  24107  lnopp2hpgb  24132  lmieu  24150  nmcfnlbi  26971  elpreq  27417  disjdifprg  27436  xrge0npcan  27684  archiabl  27742  orngsqr  27794  esumcst  28071  hasheuni  28091  esumcvg  28092  ddemeas  28208  eulerpartlemgc  28301  eulerpartlemb  28307  plymulx  28505  signswmnd  28514  signstfvneq0  28529  erdsze2lem1  28647  mrsubvrs  28882  trpredlem1  29310  wl-cbvalnaed  29985  wl-nfeqfb  29990  itg2addnclem  30066  itg2addnclem2  30067  iblmulc2nc  30080  ftc1anclem5  30094  ftc1anc  30098  dvasin  30103  areacirclem5  30111  exmid2  30499  ttac  30978  pw2f1ocnv  30979  aomclem5  31004  isnumbasgrplem3  31054  iocmbl  31180  radcnvrat  31195  dvdslcm  31204  lcmcl  31207  lcmneg  31209  lcmgcd  31213  bccbc  31250  binomcxp  31262  fnchoice  31404  fzisoeu  31500  fperiodmul  31504  upbdrech2  31508  fzdifsuc2  31512  ioondisj2  31525  iccdifprioo  31556  fsumsplitsn  31571  fmul01lt1lem1  31578  fmul01lt1lem2  31579  fprodsplitsn  31592  fprodle  31604  limciccioolb  31627  lptioo2  31637  lptioo1  31638  limcicciooub  31643  lptre2pt  31646  limcresiooub  31648  limcresioolb  31649  limcleqr  31650  coskpi2  31666  cosknegpi  31669  icccncfext  31690  cncfiooicclem1  31696  cncfiooicc  31697  cncfiooiccre  31698  dvbdfbdioolem2  31726  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnxpaek  31739  dvnprodlem1  31743  dvnprodlem3  31745  volioc  31771  itgioocnicc  31776  iblcncfioo  31777  stoweidlem14  31796  stoweidlem26  31808  stoweidlem28  31810  stoweidlem55  31837  stoweid  31845  stirlinglem5  31860  stirlinglem12  31867  dirkerper  31878  dirkertrigeqlem3  31882  dirkertrigeq  31883  dirkercncflem1  31885  dirkercncflem2  31886  dirkercncf  31889  fourierdlem10  31899  fourierdlem12  31901  fourierdlem24  31913  fourierdlem30  31919  fourierdlem31  31920  fourierdlem32  31921  fourierdlem33  31922  fourierdlem34  31923  fourierdlem35  31924  fourierdlem37  31926  fourierdlem40  31929  fourierdlem41  31930  fourierdlem42  31931  fourierdlem43  31932  fourierdlem44  31933  fourierdlem46  31935  fourierdlem48  31937  fourierdlem49  31938  fourierdlem51  31940  fourierdlem54  31943  fourierdlem62  31951  fourierdlem64  31953  fourierdlem65  31954  fourierdlem70  31959  fourierdlem71  31960  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem78  31967  fourierdlem79  31968  fourierdlem80  31969  fourierdlem81  31970  fourierdlem82  31971  fourierdlem92  31981  fourierdlem93  31982  fourierdlem97  31986  fourierdlem101  31990  fourierdlem102  31991  fourierdlem103  31992  fourierdlem104  31993  fourierdlem109  31998  fourierdlem114  32003  sqwvfoura  32011  sqwvfourb  32012  fourierswlem  32013  fouriersw  32014  elaa2lem  32016  etransclem15  32032  etransclem19  32036  etransclem20  32037  etransclem22  32039  etransclem23  32040  etransclem24  32041  etransclem25  32042  etransclem27  32044  etransclem28  32045  etransclem35  32052  etransclem38  32055  sharhght  32082  3dim1  35191  3dim2  35192  3dim3  35193  3atlem3  35209  3atlem7  35213  lvolnle3at  35306  2lplnja  35343  paddasslem18  35561  lhpexle3lem  35735  4atex  35800  cdlemd5  35927  cdleme16  36010  cdleme20  36050  cdleme21j  36062  cdleme21  36063  cdleme32snaw  36161  cdleme32fvcl  36166  cdleme32le  36173  cdlemeg46gf  36259  cdleme48gfv  36263  cdleme50trn12  36278  cdlemg6  36349  cdlemg7N  36352  cdlemg38  36441  cdlemg46  36461  dibvalrel  36890  dihlss  36977  dihglblem5aN  37019  dihmeetbN  37030  dihmeetALTN  37054  dihatlat  37061  dihatexv  37065  dvh3dim2  37175  dvh3dim3N  37176  lclkrlem2h  37241  mapdh8d  37510  mapdh8g  37513  hdmap11lem2  37572
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
  Copyright terms: Public domain W3C validator