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

Theorem eximdv 1754
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1701. (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 1748 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2eximdh 1718 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1659
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748
This theorem depends on definitions:  df-bi 188  df-ex 1660
This theorem is referenced by:  2eximdv  1756  exlimdv  1768  19.41v  1819  equviniv  1852  mo2v  2270  mo2vOLD  2271  moim  2313  reximdv2  2894  cgsexg  3111  spc3egv  3167  euind  3255  ssel  3455  reupick  3754  reximdva0  3770  uniss  4234  eusvnfb  4612  reusv2lem3  4619  coss1  5001  coss2  5002  dmss  5045  dmcosseq  5107  funssres  5632  brprcneu  5865  fv3  5885  dffv2  5945  fvn0ssdmfun  6019  dffo4  6044  dffo5  6045  fvclss  6153  fsnex  6187  f1prex  6188  f1eqcocnv  6205  mapsn  7512  enp1i  7803  en2  7804  en4  7806  marypha2  7950  brwdom3  8088  isinffi  8416  infpwfien  8482  infmap2  8637  cfub  8668  cflm  8669  cff1  8677  cfss  8684  isf32lem9  8780  axcc4  8858  acncc  8859  domtriomlem  8861  ac6s  8903  iundom2g  8954  winalim2  9110  grudomon  9231  nsmallnq  9391  prnmadd  9411  ltexprlem1  9450  ltexprlem3  9452  ltexprlem4  9453  reclem2pr  9462  dedekind  9786  xrsupsslem  11581  xrinfmsslem  11582  coss12d  13004  supcvg  13881  vdwlem2  14884  ram0  14932  mreexexlem2d  15495  initoeu1  15850  termoeu1  15857  acsmapd  16368  acsmap2d  16369  dirge  16427  odcau  17184  ablfac2  17650  lspprat  18304  cmpsub  20339  cmpcld  20341  2ndcsep  20398  1stcelcls  20400  txcn  20565  fgcl  20817  ufildom1  20865  metustexhalf  21495  bcthlem5  22182  mbfi1flim  22555  itg2seq  22574  dchrisumlem3  24189  umgraex  24893  usgraedg4  24957  wlklniswwlkn2  25270  frisusgranb  25567  frgrancvvdeqlemC  25609  ubthlem1  26354  axhcompl-zf  26483  isch3  26726  cnlnssadj  27565  acunirnmpt  28098  f1ocnt  28209  ishashinf  28214  insiga  28795  bnj605  29503  bnj607  29512  bnj1018  29558  erdsze2lem1  29711  fundmpss  30191  dissneqlem  31473  relowlpssretop  31498  poimirlem30  31674  fdc1  31779  prdstotbnd  31830  prter2  32161  lsat0cv  32308  pmapglb2N  33045  elpaddn0  33074  cdlemftr3  33841  dibglbN  34443  dihglbcpreN  34577  dihjatcclem4  34698  mapdordlem2  34914  dfac11  35630  ax6e2ndeq  36567  fnchoice  36994  rfcnnnub  37001  founiiun0  37092  fzisoeu  37131  islpcn  37295  lptre2pt  37296  stoweidlem14  37447  stoweidlem35  37469  stoweidlem39  37473  stoweidlem50  37484  stoweidlem56  37490  stoweidlem59  37493  stoweidlem60  37494  fourier2  37663  funressnfv  38033
  Copyright terms: Public domain W3C validator