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

Theorem rexlimdv3a 2640
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 2637. (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 2637 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 2517
This theorem is referenced by:  sorpssuni  6185  sorpssint  6186  tcrank  7487  rpnnen1lem5  10278  hashfun  11319  resqrex  11666  resqrcl  11669  lbsextlem3  15840  cmpsublem  17053  cmpcld  17056  ovoliunlem2  18789  isblo3i  21304  trisegint  23991  rpnnen3lem  26456  dvconstbi  26883  expgrowth  26884  lshpnelb  28304  lsatfixedN  28329  lsmsatcv  28330  lssatomic  28331  lcv1  28361  lsatcvatlem  28369  islshpcv  28373  lfl1  28390  lshpsmreu  28429  lshpkrex  28438  lshpset2N  28439  lkrlspeqN  28491  cvrval3  28732  1cvratlt  28793  ps-2b  28801  llnnleat  28832  lvolex3N  28857  lplncvrlvol2  28934  osumcllem7N  29281  lhp0lt  29322  lhpj1  29341  4atexlemex6  29393  4atexlem7  29394  trlnidat  29492  cdlemd9  29525  cdleme21h  29653  cdlemg7fvbwN  29926  cdlemg7aN  29944  cdlemg34  30031  cdlemg36  30033  cdlemg44  30052  cdlemg48  30056  tendo1ne0  30147  cdlemk26-3  30225  cdlemk55b  30279  cdleml4N  30298  dih1dimatlem0  30648  dihglblem6  30660  dochshpncl  30704  dvh4dimlem  30763  dvh3dim2  30768  dvh3dim3N  30769  dochsatshpb  30772  dochexmidlem4  30783  dochexmidlem5  30784  dochexmidlem8  30787  dochkr1  30798  dochkr1OLDN  30799  lcfl7lem  30819  lcfl6  30820  lcfl8  30822  lcfrlem16  30878  lcfrlem40  30902  mapdval2N  30950  mapdrvallem2  30965  mapdpglem24  31024  mapdh6iN  31064  mapdh8ad  31099  mapdh8e  31104  hdmap1l6i  31139  hdmapval0  31156  hdmapevec  31158  hdmapval3N  31161  hdmap10lem  31162  hdmap11lem2  31165  hdmaprnlem15N  31184  hdmaprnlem16N  31185  hdmap14lem10  31200  hdmap14lem11  31201  hdmap14lem12  31202  hdmap14lem14  31204  hgmapval0  31215  hgmapval1  31216  hgmapadd  31217  hgmapmul  31218  hgmaprnlem3N  31221  hgmaprnlem4N  31222  hgmap11  31225  hgmapvvlem3  31248
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 2520  df-rex 2521
  Copyright terms: Public domain W3C validator