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

Theorem eximdv 1711
Description: Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1655. (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 1705 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2eximdh 1674 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1613
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705
This theorem depends on definitions:  df-bi 185  df-ex 1614
This theorem is referenced by:  2eximdv  1713  exlimdv  1725  19.41v  1772  equviniv  1804  mo2v  2290  mo2vOLD  2291  mo2vOLDOLD  2292  moim  2340  reximdv2  2928  cgsexg  3142  spc3egv  3198  euind  3286  ssel  3493  reupick  3789  reximdva0  3805  uniss  4272  eusvnfb  4652  reusv2lem3  4659  reusv6OLD  4667  coss1  5168  coss2  5169  dmss  5212  dmcosseq  5274  funssres  5634  brprcneu  5865  fv3  5885  dffv2  5946  fvn0ssdmfun  6023  dffo4  6048  dffo5  6049  fvclss  6155  f1eqcocnv  6205  mapsn  7479  enp1i  7773  en2  7774  en4  7776  marypha2  7917  brwdom3  8026  isinffi  8390  infpwfien  8460  infmap2  8615  cfub  8646  cflm  8647  cff1  8655  cfss  8662  isf32lem9  8758  axcc4  8836  acncc  8837  domtriomlem  8839  ac6s  8881  iundom2g  8932  winalim2  9091  grudomon  9212  nsmallnq  9372  prnmadd  9392  ltexprlem1  9431  ltexprlem3  9433  ltexprlem4  9434  reclem2pr  9443  dedekind  9761  xrsupsslem  11523  xrinfmsslem  11524  supcvg  13678  vdwlem2  14511  ram0  14551  mreexexlem2d  15061  initoeu1  15416  termoeu1  15423  acsmapd  15934  acsmap2d  15935  dirge  15993  odcau  16750  ablfac2  17266  lspprat  17925  cmpsub  20026  cmpcld  20028  2ndcsep  20085  1stcelcls  20087  txcn  20252  fgcl  20504  ufildom1  20552  metustexhalfOLD  21191  metustexhalf  21192  bcthlem5  21892  mbfi1flim  22255  itg2seq  22274  dchrisumlem3  23801  umgraex  24449  usgraedg4  24513  wlklniswwlkn2  24826  frisusgranb  25123  frgrancvvdeqlemC  25165  ubthlem1  25912  axhcompl-zf  26041  isch3  26285  cnlnssadj  27125  acunirnmpt  27647  ishashinf  27758  insiga  28298  erdsze2lem1  28822  fundmpss  29371  fdc1  30401  prdstotbnd  30452  prter2  30784  dfac11  31170  fnchoice  31565  rfcnnnub  31572  fzisoeu  31661  islpcn  31806  lptre2pt  31807  stoweidlem14  31957  stoweidlem35  31978  stoweidlem39  31982  stoweidlem50  31993  stoweidlem56  31999  stoweidlem59  32002  stoweidlem60  32003  fourier2  32171  funressnfv  32374  ax6e2ndeq  33433  bnj605  34066  bnj607  34075  bnj1018  34121  lsat0cv  34859  pmapglb2N  35596  elpaddn0  35625  cdlemftr3  36392  dibglbN  36994  dihglbcpreN  37128  dihjatcclem4  37249  mapdordlem2  37465  coss12d  37860
  Copyright terms: Public domain W3C validator