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  27863  lsatfixedN  27888  lsmsatcv  27889  lssatomic  27890  lcv1  27920  lsatcvatlem  27928  islshpcv  27932  lfl1  27949  lshpsmreu  27988  lshpkrex  27997  lshpset2N  27998  lkrlspeqN  28050  cvrval3  28291  1cvratlt  28352  ps-2b  28360  llnnleat  28391  lvolex3N  28416  lplncvrlvol2  28493  osumcllem7N  28840  lhp0lt  28881  lhpj1  28900  4atexlemex6  28952  4atexlem7  28953  trlnidat  29051  cdlemd9  29084  cdleme21h  29212  cdlemg7fvbwN  29485  cdlemg7aN  29503  cdlemg34  29590  cdlemg36  29592  cdlemg44  29611  cdlemg48  29615  tendo1ne0  29706  cdlemk26-3  29784  cdlemk55b  29838  cdleml4N  29857  dih1dimatlem0  30207  dihglblem6  30219  dochshpncl  30263  dvh4dimlem  30322  dvh3dim2  30327  dvh3dim3N  30328  dochsatshpb  30331  dochexmidlem4  30342  dochexmidlem5  30343  dochexmidlem8  30346  dochkr1  30357  dochkr1OLDN  30358  lcfl7lem  30378  lcfl6  30379  lcfl8  30381  lcfrlem16  30437  lcfrlem40  30461  mapdval2N  30509  mapdrvallem2  30524  mapdpglem24  30583  mapdh6iN  30623  mapdh8ad  30658  mapdh8e  30663  hdmap1l6i  30698  hdmapval0  30715  hdmapevec  30717  hdmapval3N  30720  hdmap10lem  30721  hdmap11lem2  30724  hdmaprnlem15N  30743  hdmaprnlem16N  30744  hdmap14lem10  30759  hdmap14lem11  30760  hdmap14lem12  30761  hdmap14lem14  30763  hgmapval0  30774  hgmapval1  30775  hgmapadd  30776  hgmapmul  30777  hgmaprnlem3N  30780  hgmaprnlem4N  30781  hgmap11  30784  hgmapvvlem3  30807
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