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

Theorem eximdv 1676
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 1670 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2eximdh 1640 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670
This theorem depends on definitions:  df-bi 185  df-ex 1587
This theorem is referenced by:  2eximdv  1678  exlimdv  1690  equviniv  1741  mo2v  2259  mo2vOLD  2260  moim  2317  morimvOLD  2320  reximdv2  2820  cgsexg  3000  spc3egv  3056  euind  3141  ssel  3345  reupick  3629  reximdva0  3643  uniss  4107  eusvnfb  4483  reusv2lem3  4490  reusv6OLD  4498  coss1  4990  coss2  4991  dmss  5034  dmcosseq  5096  funssres  5453  brprcneu  5679  fv3  5698  dffv2  5759  dffo4  5854  dffo5  5855  fvclss  5954  f1eqcocnv  5994  mapsn  7246  enp1i  7539  en2  7540  en4  7542  marypha2  7681  brwdom3  7789  isinffi  8154  infpwfien  8224  infmap2  8379  cfub  8410  cflm  8411  cff1  8419  cfss  8426  isf32lem9  8522  axcc4  8600  acncc  8601  domtriomlem  8603  ac6s  8645  iundom2g  8696  winalim2  8855  grudomon  8976  nsmallnq  9138  prnmadd  9158  ltexprlem1  9197  ltexprlem3  9199  ltexprlem4  9200  reclem2pr  9209  dedekind  9525  xrsupsslem  11261  xrinfmsslem  11262  supcvg  13310  vdwlem2  14035  ram0  14075  mreexexlem2d  14575  acsmapd  15340  acsmap2d  15341  dirge  15399  odcau  16094  ablfac2  16578  lspprat  17211  cmpsub  18978  cmpcld  18980  2ndcsep  19038  1stcelcls  19040  txcn  19174  fgcl  19426  ufildom1  19474  metustexhalfOLD  20113  metustexhalf  20114  bcthlem5  20814  mbfi1flim  21176  itg2seq  21195  dchrisumlem3  22715  umgraex  23208  usgraedg4  23256  ubthlem1  24222  axhcompl-zf  24351  isch3  24595  cnlnssadj  25435  ishashinf  26036  insiga  26532  erdsze2lem1  27043  fundmpss  27528  fdc1  28595  prdstotbnd  28646  prter2  28979  dfac11  29368  fnchoice  29704  rfcnnnub  29711  stoweidlem14  29762  stoweidlem35  29783  stoweidlem39  29787  stoweidlem50  29798  stoweidlem56  29804  stoweidlem59  29807  stoweidlem60  29808  funressnfv  29987  wlklniswwlkn2  30287  frisusgranb  30542  frgrancvvdeqlemC  30585  ax6e2ndeq  31155  bnj605  31787  bnj607  31796  bnj1018  31842  lsat0cv  32518  pmapglb2N  33255  elpaddn0  33284  cdlemftr3  34049  dibglbN  34651  dihglbcpreN  34785  dihjatcclem4  34906  mapdordlem2  35122
  Copyright terms: Public domain W3C validator