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

Theorem eximdv 1686
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)
Hypothesis
Ref Expression
alimdv.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
eximdv  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)

Proof of Theorem eximdv
StepHypRef Expression
1 ax-5 1680 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2eximdh 1650 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-ex 1597
This theorem is referenced by:  2eximdv  1688  exlimdv  1700  equviniv  1752  mo2v  2282  mo2vOLD  2283  mo2vOLDOLD  2284  moim  2341  morimvOLD  2344  reximdv2  2934  cgsexg  3146  spc3egv  3202  euind  3290  ssel  3498  reupick  3782  reximdva0  3796  uniss  4266  eusvnfb  4643  reusv2lem3  4650  reusv6OLD  4658  coss1  5156  coss2  5157  dmss  5200  dmcosseq  5262  funssres  5626  brprcneu  5857  fv3  5877  dffv2  5938  dffo4  6035  dffo5  6036  fvclss  6140  f1eqcocnv  6190  mapsn  7457  enp1i  7751  en2  7752  en4  7754  marypha2  7895  brwdom3  8004  isinffi  8369  infpwfien  8439  infmap2  8594  cfub  8625  cflm  8626  cff1  8634  cfss  8641  isf32lem9  8737  axcc4  8815  acncc  8816  domtriomlem  8818  ac6s  8860  iundom2g  8911  winalim2  9070  grudomon  9191  nsmallnq  9351  prnmadd  9371  ltexprlem1  9410  ltexprlem3  9412  ltexprlem4  9413  reclem2pr  9422  dedekind  9739  xrsupsslem  11494  xrinfmsslem  11495  supcvg  13623  vdwlem2  14352  ram0  14392  mreexexlem2d  14893  acsmapd  15658  acsmap2d  15659  dirge  15717  odcau  16417  ablfac2  16927  lspprat  17579  cmpsub  19663  cmpcld  19665  2ndcsep  19723  1stcelcls  19725  txcn  19859  fgcl  20111  ufildom1  20159  metustexhalfOLD  20798  metustexhalf  20799  bcthlem5  21499  mbfi1flim  21862  itg2seq  21881  dchrisumlem3  23401  umgraex  23996  usgraedg4  24060  wlklniswwlkn2  24373  frisusgranb  24670  frgrancvvdeqlemC  24713  ubthlem1  25459  axhcompl-zf  25588  isch3  25832  cnlnssadj  26672  ishashinf  27271  insiga  27774  erdsze2lem1  28284  fundmpss  28770  fdc1  29840  prdstotbnd  29891  prter2  30224  dfac11  30612  fnchoice  30982  rfcnnnub  30989  fzisoeu  31077  islpcn  31181  lptre2pt  31182  stoweidlem14  31314  stoweidlem35  31335  stoweidlem39  31339  stoweidlem50  31350  stoweidlem56  31356  stoweidlem59  31359  stoweidlem60  31360  fourier2  31528  funressnfv  31680  iopmapxp  31960  ax6e2ndeq  32412  bnj605  33044  bnj607  33053  bnj1018  33099  lsat0cv  33830  pmapglb2N  34567  elpaddn0  34596  cdlemftr3  35361  dibglbN  35963  dihglbcpreN  36097  dihjatcclem4  36218  mapdordlem2  36434  coss12d  36779
  Copyright terms: Public domain W3C validator