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

Theorem rexlimd 2947
Description: Deduction from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 14-Jan-2020.)
Hypotheses
Ref Expression
rexlimd.1  |-  F/ x ph
rexlimd.2  |-  F/ x ch
rexlimd.3  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
Assertion
Ref Expression
rexlimd  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )

Proof of Theorem rexlimd
StepHypRef Expression
1 rexlimd.1 . 2  |-  F/ x ph
2 rexlimd.2 . . 3  |-  F/ x ch
32a1i 11 . 2  |-  ( ph  ->  F/ x ch )
4 rexlimd.3 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
51, 3, 4rexlimd2 2946 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   F/wnf 1599    e. wcel 1767   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600  df-ral 2819  df-rex 2820
This theorem is referenced by:  rexlimdvOLD  2954  reusv2lem2  4649  reusv6OLD  4658  ralxfrALT  4666  fvmptt  5963  ffnfv  6045  peano5  6701  tz7.49  7107  nneneq  7697  ac6sfi  7760  ixpiunwdom  8013  r1val1  8200  rankuni2b  8267  infpssrlem4  8682  zorn2lem4  8875  zorn2lem5  8876  konigthlem  8939  tskuni  9157  gruiin  9184  lbzbi  11166  iunconlem  19694  ptbasfi  19817  alexsubALTlem3  20284  ovoliunnul  21653  iunmbl2  21702  mptelee  23874  atom1d  26948  elabreximd  27082  iundisjf  27121  esumc  27702  heicant  29626  indexa  29827  sdclem2  29838  refsumcn  30983  suprnmpt  31029  upbdrech  31082  ssfiunibd  31086  iccshift  31122  iooshift  31126  fmul01lt1  31136  islptre  31161  rexlim2d  31167  limcperiod  31170  islpcn  31181  limclner  31193  dvbdfbdioolem1  31258  itgiccshift  31298  itgperiod  31299  stoweidlem29  31329  stoweidlem31  31331  stoweidlem59  31359  stirlinglem13  31386  fourierdlem48  31455  fourierdlem51  31458  fourierdlem53  31460  fourierdlem80  31487  fourierdlem81  31488  fourierdlem93  31500  ffnafv  31723  glbconxN  34174  cdleme26ee  35156  cdleme32d  35240  cdleme32f  35242  cdlemk38  35711  cdlemk19x  35739  cdlemk11t  35742
  Copyright terms: Public domain W3C validator