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

Theorem eximdv 1710
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1654. (Contributed by NM, 27-Apr-1994.)
Hypothesis
Ref Expression
alimdv.1
Assertion
Ref Expression
eximdv
Distinct variable group:   ,

Proof of Theorem eximdv
StepHypRef Expression
1 ax-5 1704 . 2
2 alimdv.1 . 2
31, 2eximdh 1673 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  E.wex 1612
This theorem is referenced by:  2eximdv  1712  exlimdv  1724  19.41v  1771  equviniv  1803  mo2v  2289  mo2vOLD  2290  mo2vOLDOLD  2291  moim  2339  morimvOLD  2342  reximdv2  2928  cgsexg  3142  spc3egv  3198  euind  3286  ssel  3497  reupick  3781  reximdva0  3796  uniss  4270  eusvnfb  4648  reusv2lem3  4655  reusv6OLD  4663  coss1  5163  coss2  5164  dmss  5207  dmcosseq  5269  funssres  5633  brprcneu  5864  fv3  5884  dffv2  5946  fvn0ssdmfun  6022  dffo4  6047  dffo5  6048  fvclss  6154  f1eqcocnv  6204  mapsn  7480  enp1i  7775  en2  7776  en4  7778  marypha2  7919  brwdom3  8029  isinffi  8394  infpwfien  8464  infmap2  8619  cfub  8650  cflm  8651  cff1  8659  cfss  8666  isf32lem9  8762  axcc4  8840  acncc  8841  domtriomlem  8843  ac6s  8885  iundom2g  8936  winalim2  9095  grudomon  9216  nsmallnq  9376  prnmadd  9396  ltexprlem1  9435  ltexprlem3  9437  ltexprlem4  9438  reclem2pr  9447  dedekind  9765  xrsupsslem  11527  xrinfmsslem  11528  supcvg  13667  vdwlem2  14500  ram0  14540  mreexexlem2d  15042  acsmapd  15808  acsmap2d  15809  dirge  15867  odcau  16624  ablfac2  17140  lspprat  17799  cmpsub  19900  cmpcld  19902  2ndcsep  19960  1stcelcls  19962  txcn  20127  fgcl  20379  ufildom1  20427  metustexhalfOLD  21066  metustexhalf  21067  bcthlem5  21767  mbfi1flim  22130  itg2seq  22149  dchrisumlem3  23676  umgraex  24323  usgraedg4  24387  wlklniswwlkn2  24700  frisusgranb  24997  frgrancvvdeqlemC  25039  ubthlem1  25786  axhcompl-zf  25915  isch3  26159  cnlnssadj  26999  ishashinf  27606  insiga  28137  erdsze2lem1  28647  fundmpss  29196  fdc1  30239  prdstotbnd  30290  prter2  30622  dfac11  31008  fnchoice  31404  rfcnnnub  31411  fzisoeu  31500  islpcn  31645  lptre2pt  31646  stoweidlem14  31796  stoweidlem35  31817  stoweidlem39  31821  stoweidlem50  31832  stoweidlem56  31838  stoweidlem59  31841  stoweidlem60  31842  fourier2  32010  funressnfv  32213  initoeu1  32617  termoeu1  32624  ax6e2ndeq  33332  bnj605  33965  bnj607  33974  bnj1018  34020  lsat0cv  34758  pmapglb2N  35495  elpaddn0  35524  cdlemftr3  36291  dibglbN  36893  dihglbcpreN  37027  dihjatcclem4  37148  mapdordlem2  37364  coss12d  37759
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator