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

Theorem rexlimdv3a 2631
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 2628. (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 2628 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 2510
This theorem is referenced by:  sorpssuni  6138  sorpssint  6139  tcrank  7438  rpnnen1lem5  10225  hashfun  11266  resqrex  11613  resqrcl  11616  lbsextlem3  15745  cmpsublem  16958  cmpcld  16961  ovoliunlem2  18694  isblo3i  21209  trisegint  23825  rpnnen3lem  26290  dvconstbi  26717  expgrowth  26718  lshpnelb  27975  lsatfixedN  28000  lsmsatcv  28001  lssatomic  28002  lcv1  28032  lsatcvatlem  28040  islshpcv  28044  lfl1  28061  lshpsmreu  28100  lshpkrex  28109  lshpset2N  28110  lkrlspeqN  28162  cvrval3  28403  1cvratlt  28464  ps-2b  28472  llnnleat  28503  lvolex3N  28528  lplncvrlvol2  28605  osumcllem7N  28952  lhp0lt  28993  lhpj1  29012  4atexlemex6  29064  4atexlem7  29065  trlnidat  29163  cdlemd9  29196  cdleme21h  29324  cdlemg7fvbwN  29597  cdlemg7aN  29615  cdlemg34  29702  cdlemg36  29704  cdlemg44  29723  cdlemg48  29727  tendo1ne0  29818  cdlemk26-3  29896  cdlemk55b  29950  cdleml4N  29969  dih1dimatlem0  30319  dihglblem6  30331  dochshpncl  30375  dvh4dimlem  30434  dvh3dim2  30439  dvh3dim3N  30440  dochsatshpb  30443  dochexmidlem4  30454  dochexmidlem5  30455  dochexmidlem8  30458  dochkr1  30469  dochkr1OLDN  30470  lcfl7lem  30490  lcfl6  30491  lcfl8  30493  lcfrlem16  30549  lcfrlem40  30573  mapdval2N  30621  mapdrvallem2  30636  mapdpglem24  30695  mapdh6iN  30735  mapdh8ad  30770  mapdh8e  30775  hdmap1l6i  30810  hdmapval0  30827  hdmapevec  30829  hdmapval3N  30832  hdmap10lem  30833  hdmap11lem2  30836  hdmaprnlem15N  30855  hdmaprnlem16N  30856  hdmap14lem10  30871  hdmap14lem11  30872  hdmap14lem12  30873  hdmap14lem14  30875  hgmapval0  30886  hgmapval1  30887  hgmapadd  30888  hgmapmul  30889  hgmaprnlem3N  30892  hgmaprnlem4N  30893  hgmap11  30896  hgmapvvlem3  30919
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 2513  df-rex 2514
  Copyright terms: Public domain W3C validator