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

Theorem rexlimdv3a 2644
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 2641. (Contributed by NM, 7-Jun-2015.)
Hypothesis
Ref Expression
rexlimdv3a.1  |-  ( (
ph  /\  x  e.  A  /\  ps )  ->  ch )
Assertion
Ref Expression
rexlimdv3a  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Distinct variable groups:    ph, x    ch, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem rexlimdv3a
StepHypRef Expression
1 rexlimdv3a.1 . . 3  |-  ( (
ph  /\  x  e.  A  /\  ps )  ->  ch )
213exp 1155 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32rexlimdv 2641 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ w3a 939    e. wcel 1621   E.wrex 2519
This theorem is referenced by:  sorpssuni  6220  sorpssint  6221  tcrank  7522  rpnnen1lem5  10314  hashfun  11355  resqrex  11702  resqrcl  11705  lbsextlem3  15876  cmpsublem  17089  cmpcld  17092  ovoliunlem2  18825  isblo3i  21340  trisegint  24027  rpnnen3lem  26492  dvconstbi  26919  expgrowth  26920  lshpnelb  28424  lsatfixedN  28449  lsmsatcv  28450  lssatomic  28451  lcv1  28481  lsatcvatlem  28489  islshpcv  28493  lfl1  28510  lshpsmreu  28549  lshpkrex  28558  lshpset2N  28559  lkrlspeqN  28611  cvrval3  28852  1cvratlt  28913  ps-2b  28921  llnnleat  28952  lvolex3N  28977  lplncvrlvol2  29054  osumcllem7N  29401  lhp0lt  29442  lhpj1  29461  4atexlemex6  29513  4atexlem7  29514  trlnidat  29612  cdlemd9  29645  cdleme21h  29773  cdlemg7fvbwN  30046  cdlemg7aN  30064  cdlemg34  30151  cdlemg36  30153  cdlemg44  30172  cdlemg48  30176  tendo1ne0  30267  cdlemk26-3  30345  cdlemk55b  30399  cdleml4N  30418  dih1dimatlem0  30768  dihglblem6  30780  dochshpncl  30824  dvh4dimlem  30883  dvh3dim2  30888  dvh3dim3N  30889  dochsatshpb  30892  dochexmidlem4  30903  dochexmidlem5  30904  dochexmidlem8  30907  dochkr1  30918  dochkr1OLDN  30919  lcfl7lem  30939  lcfl6  30940  lcfl8  30942  lcfrlem16  30998  lcfrlem40  31022  mapdval2N  31070  mapdrvallem2  31085  mapdpglem24  31144  mapdh6iN  31184  mapdh8ad  31219  mapdh8e  31224  hdmap1l6i  31259  hdmapval0  31276  hdmapevec  31278  hdmapval3N  31281  hdmap10lem  31282  hdmap11lem2  31285  hdmaprnlem15N  31304  hdmaprnlem16N  31305  hdmap14lem10  31320  hdmap14lem11  31321  hdmap14lem12  31322  hdmap14lem14  31324  hgmapval0  31335  hgmapval1  31336  hgmapadd  31337  hgmapmul  31338  hgmaprnlem3N  31341  hgmaprnlem4N  31342  hgmap11  31345  hgmapvvlem3  31368
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 941  df-ex 1538  df-nf 1540  df-ral 2523  df-rex 2524
  Copyright terms: Public domain W3C validator