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

Theorem eximdv 1763
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1705. (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 1757 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2eximdh 1723 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757
This theorem depends on definitions:  df-bi 189  df-ex 1663
This theorem is referenced by:  2eximdv  1765  exlimdv  1778  19.41v  1829  equviniv  1871  mo2v  2305  moim  2347  reximdv2  2857  cgsexg  3079  spc3egv  3137  euind  3224  ssel  3425  reupick  3726  reximdva0  3742  uniss  4218  eusvnfb  4598  reusv2lem3  4605  coss1  4989  coss2  4990  dmss  5033  dmcosseq  5095  funssres  5621  brprcneu  5856  fv3  5876  dffv2  5936  fvn0ssdmfun  6011  dffo4  6036  dffo5  6037  fvclss  6145  fsnex  6179  f1prex  6180  f1eqcocnv  6197  mapsn  7510  enp1i  7803  en2  7804  en4  7806  marypha2  7950  brwdom3  8094  isinffi  8423  infpwfien  8490  infmap2  8645  cfub  8676  cflm  8677  cff1  8685  cfss  8692  isf32lem9  8788  axcc4  8866  acncc  8867  domtriomlem  8869  ac6s  8911  iundom2g  8962  winalim2  9118  grudomon  9239  nsmallnq  9399  prnmadd  9419  ltexprlem1  9458  ltexprlem3  9460  ltexprlem4  9461  reclem2pr  9470  dedekind  9794  xrsupsslem  11589  xrinfmsslem  11590  ishashinf  12623  coss12d  13029  supcvg  13907  vdwlem2  14925  ram0  14973  mreexexlem2d  15544  initoeu1  15899  termoeu1  15906  acsmapd  16417  acsmap2d  16418  dirge  16476  odcau  17249  ablfac2  17715  lspprat  18369  cmpsub  20408  cmpcld  20410  2ndcsep  20467  1stcelcls  20469  txcn  20634  fgcl  20886  ufildom1  20934  metustexhalf  21564  bcthlem5  22289  mbfi1flim  22674  itg2seq  22693  dchrisumlem3  24322  umgraex  25043  usgraedg4  25107  wlklniswwlkn2  25421  frisusgranb  25718  frgrancvvdeqlemC  25760  ubthlem1  26505  axhcompl-zf  26644  isch3  26887  cnlnssadj  27726  acunirnmpt  28254  f1ocnt  28369  insiga  28952  bnj605  29711  bnj607  29720  bnj1018  29766  erdsze2lem1  29919  fundmpss  30400  dissneqlem  31735  relowlpssretop  31760  poimirlem30  31963  fdc1  32068  prdstotbnd  32119  prter2  32447  lsat0cv  32593  pmapglb2N  33330  elpaddn0  33359  cdlemftr3  34126  dibglbN  34728  dihglbcpreN  34862  dihjatcclem4  34983  mapdordlem2  35199  dfac11  35914  ax6e2ndeq  36920  fnchoice  37344  rfcnnnub  37351  founiiun0  37459  mapsnd  37470  fzisoeu  37512  islpcn  37713  lptre2pt  37714  stoweidlem14  37868  stoweidlem35  37890  stoweidlem39  37894  stoweidlem50  37905  stoweidlem56  37911  stoweidlem59  37914  stoweidlem60  37915  fourier2  38085  qndenserrnbllem  38157  qndenserrn  38162  ovncvrrp  38380  ovnsubaddlem2  38387  hoidmvval0b  38406  hoiqssbllem3  38440  funressnfv  38623  ssrelrn  39006  funopsn  39012  upgrex  39170  uhgrvd00  39554
  Copyright terms: Public domain W3C validator