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

Theorem eximdv 1677
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 1671 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2eximdh 1641 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671
This theorem depends on definitions:  df-bi 185  df-ex 1588
This theorem is referenced by:  2eximdv  1679  exlimdv  1691  equviniv  1743  mo2v  2269  mo2vOLD  2270  mo2vOLDOLD  2271  moim  2328  morimvOLD  2331  reximdv2  2931  cgsexg  3111  spc3egv  3167  euind  3253  ssel  3459  reupick  3743  reximdva0  3757  uniss  4221  eusvnfb  4597  reusv2lem3  4604  reusv6OLD  4612  coss1  5104  coss2  5105  dmss  5148  dmcosseq  5210  funssres  5567  brprcneu  5793  fv3  5813  dffv2  5874  dffo4  5969  dffo5  5970  fvclss  6069  f1eqcocnv  6109  mapsn  7365  enp1i  7659  en2  7660  en4  7662  marypha2  7801  brwdom3  7909  isinffi  8274  infpwfien  8344  infmap2  8499  cfub  8530  cflm  8531  cff1  8539  cfss  8546  isf32lem9  8642  axcc4  8720  acncc  8721  domtriomlem  8723  ac6s  8765  iundom2g  8816  winalim2  8975  grudomon  9096  nsmallnq  9258  prnmadd  9278  ltexprlem1  9317  ltexprlem3  9319  ltexprlem4  9320  reclem2pr  9329  dedekind  9645  xrsupsslem  11381  xrinfmsslem  11382  supcvg  13437  vdwlem2  14162  ram0  14202  mreexexlem2d  14703  acsmapd  15468  acsmap2d  15469  dirge  15527  odcau  16225  ablfac2  16713  lspprat  17358  cmpsub  19136  cmpcld  19138  2ndcsep  19196  1stcelcls  19198  txcn  19332  fgcl  19584  ufildom1  19632  metustexhalfOLD  20271  metustexhalf  20272  bcthlem5  20972  mbfi1flim  21335  itg2seq  21354  dchrisumlem3  22874  umgraex  23410  usgraedg4  23458  ubthlem1  24424  axhcompl-zf  24553  isch3  24797  cnlnssadj  25637  ishashinf  26231  insiga  26726  erdsze2lem1  27236  fundmpss  27722  fdc1  28791  prdstotbnd  28842  prter2  29175  dfac11  29564  fnchoice  29900  rfcnnnub  29907  stoweidlem14  29958  stoweidlem35  29979  stoweidlem39  29983  stoweidlem50  29994  stoweidlem56  30000  stoweidlem59  30003  stoweidlem60  30004  funressnfv  30183  wlklniswwlkn2  30483  frisusgranb  30738  frgrancvvdeqlemC  30781  ax6e2ndeq  31601  bnj605  32233  bnj607  32242  bnj1018  32288  lsat0cv  33017  pmapglb2N  33754  elpaddn0  33783  cdlemftr3  34548  dibglbN  35150  dihglbcpreN  35284  dihjatcclem4  35405  mapdordlem2  35621
  Copyright terms: Public domain W3C validator