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

Theorem rexlimdv3a 2775
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 2772. (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 1152 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32rexlimdv 2772 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936    e. wcel 1717   E.wrex 2650
This theorem is referenced by:  sorpssuni  6467  sorpssint  6468  tcrank  7741  rpnnen1lem5  10536  hashfun  11627  resqrex  11983  resqrcl  11986  lbsextlem3  16159  cmpsublem  17384  cmpcld  17387  ovoliunlem2  19266  isblo3i  22150  trisegint  25676  itg2addnclem  25957  itg2addnc  25959  areacirclem4  25984  rpnnen3lem  26793  dvconstbi  27220  expgrowth  27221  stoweidlem57  27474  sigarcol  27522  lshpnelb  29099  lsatfixedN  29124  lsmsatcv  29125  lssatomic  29126  lcv1  29156  lsatcvatlem  29164  islshpcv  29168  lfl1  29185  lshpsmreu  29224  lshpkrex  29233  lshpset2N  29234  lkrlspeqN  29286  cvrval3  29527  1cvratlt  29588  ps-2b  29596  llnnleat  29627  lvolex3N  29652  lplncvrlvol2  29729  osumcllem7N  30076  lhp0lt  30117  lhpj1  30136  4atexlemex6  30188  4atexlem7  30189  trlnidat  30287  cdlemd9  30320  cdleme21h  30448  cdlemg7fvbwN  30721  cdlemg7aN  30739  cdlemg34  30826  cdlemg36  30828  cdlemg44  30847  cdlemg48  30851  tendo1ne0  30942  cdlemk26-3  31020  cdlemk55b  31074  cdleml4N  31093  dih1dimatlem0  31443  dihglblem6  31455  dochshpncl  31499  dvh4dimlem  31558  dvh3dim2  31563  dvh3dim3N  31564  dochsatshpb  31567  dochexmidlem4  31578  dochexmidlem5  31579  dochexmidlem8  31582  dochkr1  31593  dochkr1OLDN  31594  lcfl7lem  31614  lcfl6  31615  lcfl8  31617  lcfrlem16  31673  lcfrlem40  31697  mapdval2N  31745  mapdrvallem2  31760  mapdpglem24  31819  mapdh6iN  31859  mapdh8ad  31894  mapdh8e  31899  hdmap1l6i  31934  hdmapval0  31951  hdmapevec  31953  hdmapval3N  31956  hdmap10lem  31957  hdmap11lem2  31960  hdmaprnlem15N  31979  hdmaprnlem16N  31980  hdmap14lem10  31995  hdmap14lem11  31996  hdmap14lem12  31997  hdmap14lem14  31999  hgmapval0  32010  hgmapval1  32011  hgmapadd  32012  hgmapmul  32013  hgmaprnlem3N  32016  hgmaprnlem4N  32017  hgmap11  32020  hgmapvvlem3  32043
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-ex 1548  df-nf 1551  df-ral 2654  df-rex 2655
  Copyright terms: Public domain W3C validator