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

Theorem rexlimdv3a 2671
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 2668. (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 2668 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934    e. wcel 1686   E.wrex 2546
This theorem is referenced by:  sorpssuni  6288  sorpssint  6289  tcrank  7556  rpnnen1lem5  10348  hashfun  11391  resqrex  11738  resqrcl  11741  lbsextlem3  15915  cmpsublem  17128  cmpcld  17131  ovoliunlem2  18864  isblo3i  21381  trisegint  24653  itg2addnclem  24933  itg2addnc  24935  areacirclem4  24938  rpnnen3lem  27135  dvconstbi  27562  expgrowth  27563  sigarcol  27865  lshpnelb  29247  lsatfixedN  29272  lsmsatcv  29273  lssatomic  29274  lcv1  29304  lsatcvatlem  29312  islshpcv  29316  lfl1  29333  lshpsmreu  29372  lshpkrex  29381  lshpset2N  29382  lkrlspeqN  29434  cvrval3  29675  1cvratlt  29736  ps-2b  29744  llnnleat  29775  lvolex3N  29800  lplncvrlvol2  29877  osumcllem7N  30224  lhp0lt  30265  lhpj1  30284  4atexlemex6  30336  4atexlem7  30337  trlnidat  30435  cdlemd9  30468  cdleme21h  30596  cdlemg7fvbwN  30869  cdlemg7aN  30887  cdlemg34  30974  cdlemg36  30976  cdlemg44  30995  cdlemg48  30999  tendo1ne0  31090  cdlemk26-3  31168  cdlemk55b  31222  cdleml4N  31241  dih1dimatlem0  31591  dihglblem6  31603  dochshpncl  31647  dvh4dimlem  31706  dvh3dim2  31711  dvh3dim3N  31712  dochsatshpb  31715  dochexmidlem4  31726  dochexmidlem5  31727  dochexmidlem8  31730  dochkr1  31741  dochkr1OLDN  31742  lcfl7lem  31762  lcfl6  31763  lcfl8  31765  lcfrlem16  31821  lcfrlem40  31845  mapdval2N  31893  mapdrvallem2  31908  mapdpglem24  31967  mapdh6iN  32007  mapdh8ad  32042  mapdh8e  32047  hdmap1l6i  32082  hdmapval0  32099  hdmapevec  32101  hdmapval3N  32104  hdmap10lem  32105  hdmap11lem2  32108  hdmaprnlem15N  32127  hdmaprnlem16N  32128  hdmap14lem10  32143  hdmap14lem11  32144  hdmap14lem12  32145  hdmap14lem14  32147  hgmapval0  32158  hgmapval1  32159  hgmapadd  32160  hgmapmul  32161  hgmaprnlem3N  32164  hgmaprnlem4N  32165  hgmap11  32168  hgmapvvlem3  32191
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-11 1717
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-ex 1531  df-nf 1534  df-ral 2550  df-rex 2551
  Copyright terms: Public domain W3C validator