ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rexlimdva Unicode version

Theorem rexlimdva 2450
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)
Hypothesis
Ref Expression
rexlimdva.1  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
rexlimdva  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Distinct variable groups:    ph, x    ch, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem rexlimdva
StepHypRef Expression
1 rexlimdva.1 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
21ex 112 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32rexlimdv 2449 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    e. wcel 1409   E.wrex 2324
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-i5r 1444
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-ral 2328  df-rex 2329
This theorem is referenced by:  rexlimdvaa  2451  rexlimivv  2455  rexlimdvv  2456  ralxfrd  4222  rexxfrd  4223  fvelimab  5257  foco2  5346  elunirn  5433  f1elima  5440  tfrlem5  5961  tfrlemibacc  5971  tfrlemibfn  5973  nnaordex  6131  nnawordex  6132  ectocld  6203  phpm  6358  fin0  6373  fin0or  6374  supisoex  6413  ltexnqq  6564  ltbtwnnqq  6571  prarloclem4  6654  prarloc2  6660  genprndl  6677  genprndu  6678  prmuloc2  6723  1idprl  6746  1idpru  6747  cauappcvgprlemdisj  6807  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  caucvgprlemladdrl  6834  recexgt0sr  6916  nntopi  7026  cnegexlem1  7249  cnegexlem2  7250  renegcl  7335  qmulz  8655  icc0r  8896  qbtwnzlemstep  9205  rebtwn2zlemstep  9209  ioo0  9216  ico0  9218  ioc0  9219  modqmuladd  9316  addmodlteq  9348  frec2uzrand  9355  frecuzrdgfn  9362  shftlem  9645  caucvgre  9808  resqrexlemgt0  9847  climuni  10045  climshftlemg  10054  climcn1  10060  serif0  10102  dvds1lem  10119  odd2np1lem  10183  odd2np1  10184  sqoddm1div8z  10198  ltoddhalfle  10205  halfleoddlt  10206  m1expo  10212  divalglemeunn  10233  divalglemex  10234  divalglemeuneg  10235  flodddiv4  10246
  Copyright terms: Public domain W3C validator