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

Theorem rexlimdv3a 2745
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 2742. (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 1150 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32rexlimdv 2742 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934    e. wcel 1710   E.wrex 2620
This theorem is referenced by:  sorpssuni  6373  sorpssint  6374  tcrank  7644  rpnnen1lem5  10438  hashfun  11485  resqrex  11832  resqrcl  11835  lbsextlem3  16012  cmpsublem  17232  cmpcld  17235  ovoliunlem2  18966  isblo3i  21493  trisegint  25210  itg2addnclem  25492  itg2addnc  25494  areacirclem4  25519  rpnnen3lem  26447  dvconstbi  26874  expgrowth  26875  sigarcol  27177  lshpnelb  29243  lsatfixedN  29268  lsmsatcv  29269  lssatomic  29270  lcv1  29300  lsatcvatlem  29308  islshpcv  29312  lfl1  29329  lshpsmreu  29368  lshpkrex  29377  lshpset2N  29378  lkrlspeqN  29430  cvrval3  29671  1cvratlt  29732  ps-2b  29740  llnnleat  29771  lvolex3N  29796  lplncvrlvol2  29873  osumcllem7N  30220  lhp0lt  30261  lhpj1  30280  4atexlemex6  30332  4atexlem7  30333  trlnidat  30431  cdlemd9  30464  cdleme21h  30592  cdlemg7fvbwN  30865  cdlemg7aN  30883  cdlemg34  30970  cdlemg36  30972  cdlemg44  30991  cdlemg48  30995  tendo1ne0  31086  cdlemk26-3  31164  cdlemk55b  31218  cdleml4N  31237  dih1dimatlem0  31587  dihglblem6  31599  dochshpncl  31643  dvh4dimlem  31702  dvh3dim2  31707  dvh3dim3N  31708  dochsatshpb  31711  dochexmidlem4  31722  dochexmidlem5  31723  dochexmidlem8  31726  dochkr1  31737  dochkr1OLDN  31738  lcfl7lem  31758  lcfl6  31759  lcfl8  31761  lcfrlem16  31817  lcfrlem40  31841  mapdval2N  31889  mapdrvallem2  31904  mapdpglem24  31963  mapdh6iN  32003  mapdh8ad  32038  mapdh8e  32043  hdmap1l6i  32078  hdmapval0  32095  hdmapevec  32097  hdmapval3N  32100  hdmap10lem  32101  hdmap11lem2  32104  hdmaprnlem15N  32123  hdmaprnlem16N  32124  hdmap14lem10  32139  hdmap14lem11  32140  hdmap14lem12  32141  hdmap14lem14  32143  hgmapval0  32154  hgmapval1  32155  hgmapadd  32156  hgmapmul  32157  hgmaprnlem3N  32160  hgmaprnlem4N  32161  hgmap11  32164  hgmapvvlem3  32187
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-ex 1542  df-nf 1545  df-ral 2624  df-rex 2625
  Copyright terms: Public domain W3C validator