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

Theorem eximdv 1629
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-17 1623 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2eximdh 1595 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1547
This theorem is referenced by:  2eximdv  1631  exlimdv  1643  ax12olem2OLD  1966  moim  2284  morimv  2286  reximdv2  2758  cgsexg  2930  spc3egv  2983  euind  3064  ssel  3285  reupick  3568  reximdva0  3582  uniss  3978  eusvnfb  4659  reusv2lem3  4666  reusv6OLD  4674  coss1  4968  coss2  4969  dmss  5009  dmcosseq  5077  funssres  5433  brprcneu  5661  fv3  5684  dffv2  5735  dffo4  5824  dffo5  5825  fvclss  5919  f1eqcocnv  5967  mapsn  6991  enp1i  7279  en2  7280  en4  7282  marypha2  7379  brwdom3  7483  isinffi  7812  infpwfien  7876  infmap2  8031  cfub  8062  cflm  8063  cff1  8071  cfss  8078  isf32lem9  8174  axcc4  8252  acncc  8253  domtriomlem  8255  ac6s  8297  iundom2g  8348  winalim2  8504  grudomon  8625  nsmallnq  8787  prnmadd  8807  ltexprlem1  8846  ltexprlem3  8848  ltexprlem4  8849  reclem2pr  8858  xrsupsslem  10817  xrinfmsslem  10818  supcvg  12562  vdwlem2  13277  ram0  13317  mreexexlem2d  13797  acsmapd  14531  acsmap2d  14532  dirge  14609  odcau  15165  ablfac2  15574  lspprat  16152  cmpsub  17385  cmpcld  17387  2ndcsep  17443  1stcelcls  17445  txcn  17579  fgcl  17831  ufildom1  17879  metustexhalf  18476  bcthlem5  19150  mbfi1flim  19482  itg2seq  19501  dchrisumlem3  21052  umgraex  21225  usgraedg4  21272  ubthlem1  22220  axhcompl-zf  22349  isch3  22592  cnlnssadj  23431  ishashinf  23997  insiga  24316  erdsze2lem1  24668  dedekind  24966  fundmpss  25146  fdc1  26141  prdstotbnd  26194  prter2  26421  dfac11  26829  fnchoice  27368  rfcnnnub  27375  stoweidlem14  27431  stoweidlem27  27444  stoweidlem35  27452  stoweidlem39  27456  stoweidlem50  27467  stoweidlem56  27473  stoweidlem59  27476  stoweidlem60  27477  funressnfv  27661  frisusgranb  27750  frgrancvvdeqlemC  27791  a9e2ndeq  27989  bnj605  28616  bnj607  28625  bnj1018  28671  ax12olem2wAUX7  28794  ax12olem2OLD7  29022  lsat0cv  29148  pmapglb2N  29885  elpaddn0  29914  cdlemftr3  30679  dibglbN  31281  dihglbcpreN  31415  dihjatcclem4  31536  mapdordlem2  31752
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator