Theorem eximdv 1846

Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1761. (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

Step	Hyp	Ref	Expression
1		ax-5 1839	. 2 |- ( ph -> A. x ph )
2		alimdv.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	eximdh 1791	1 |- ( ph -> ( E. x ps -> E. x ch ) )

Syntax hints:   -> wi 4   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  2eximdv  1848  exlimdv  1861  19.41v  1914  equvinv  1959  equviniva  1960  equvinivOLD  1961  mo2v  2477  moim  2519  reximdv2  3014  cgsexg  3238  spc3egv  3297  euind  3393  ssel  3597  reupick  3911  reximdva0  3933  uniss  4458  eusvnfb  4862  reusv2lem3  4871  relopabi  5245  coss1  5277  coss2  5278  ssrelrn  5315  dmss  5323  dmcosseq  5387  funssres  5930  brprcneu  6184  fv3  6206  dffv2  6271  fvn0ssdmfun  6350  dffo4  6375  dffo5  6376  funopsn  6413  fvclss  6500  fsnex  6538  f1prex  6539  f1eqcocnv  6556  mapsn  7899  enp1i  8195  en2  8196  en4  8198  marypha2  8345  brwdom3  8487  isinffi  8818  infpwfien  8885  infmap2  9040  cfub  9071  cflm  9072  cff1  9080  cfss  9087  isf32lem9  9183  axcc4  9261  acncc  9262  domtriomlem  9264  ac6s  9306  iundom2g  9362  winalim2  9518  grudomon  9639  nsmallnq  9799  prnmadd  9819  ltexprlem1  9858  ltexprlem3  9860  ltexprlem4  9861  reclem2pr  9870  dedekind  10200  xrsupsslem  12137  xrinfmsslem  12138  ishashinf  13247  coss12d  13711  supcvg  14588  vdwlem2  15686  ram0  15726  mreexexlem2d  16305  initoeu1  16661  termoeu1  16668  acsmapd  17178  acsmap2d  17179  dirge  17237  odcau  18019  ablfac2  18488  lspprat  19153  cmpsub  21203  cmpcld  21205  2ndcsep  21262  1stcelcls  21264  txcn  21429  fgcl  21682  ufildom1  21730  metustexhalf  22361  bcthlem5  23125  mbfi1flim  23490  itg2seq  23509  dchrisumlem3  25180  upgrex  25987  uhgrvd00  26430  wlkiswwlksupgr2  26763  wlklnwwlkln2lem  26768  umgrwwlks2on  26850  wpthswwlks2on  26854  frcond3  27133  frgrncvvdeqlem9  27171  ubthlem1  27726  axhcompl-zf  27855  isch3  28098  cnlnssadj  28939  acunirnmpt  29459  f1ocnt  29559  insiga  30200  bnj605  30977  bnj607  30986  bnj1018  31032  erdsze2lem1  31185  fundmpss  31664  bj-restn0  33043  dissneqlem  33187  relowlpssretop  33212  poimirlem30  33439  fdc1  33542  prdstotbnd  33593  prter2  34166  lsat0cv  34320  pmapglb2N  35057  elpaddn0  35086  cdlemftr3  35853  dibglbN  36455  dihglbcpreN  36589  dihjatcclem4  36710  mapdordlem2  36926  dfac11  37632  neik0pk1imk0  38345  ax6e2ndeq  38775  fnchoice  39188  rfcnnnub  39195  eliin2f  39287  founiiun0  39377  mapsnd  39388  axccd  39429  axccd2  39430  fvelima2  39475  fzisoeu  39514  islpcn  39871  lptre2pt  39872  stoweidlem14  40231  stoweidlem35  40252  stoweidlem39  40256  stoweidlem50  40267  stoweidlem56  40273  stoweidlem59  40276  stoweidlem60  40277  fourier2  40444  qndenserrnbllem  40514  qndenserrn  40519  ovncvrrp  40778  ovnsubaddlem2  40785  hoidmvval0b  40804  hoiqssbllem3  40838  funressnfv  41208  elsprel  41725