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

Theorem rexlimdv3a 3180
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 3177. (Contributed by NM, 7-Jun-2015.)
Hypothesis
Ref Expression
rexlimdv3a.1 ((𝜑𝑥𝐴𝜓) → 𝜒)
Assertion
Ref Expression
rexlimdv3a (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Distinct variable groups:   𝜑,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimdv3a
StepHypRef Expression
1 rexlimdv3a.1 . . 3 ((𝜑𝑥𝐴𝜓) → 𝜒)
213exp 1148 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32rexlimdv 3177 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1107  wcel 2155  wrex 3056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005
This theorem depends on definitions:  df-bi 198  df-an 385  df-3an 1109  df-ex 1875  df-ral 3060  df-rex 3061
This theorem is referenced by:  sorpssuni  7144  sorpssint  7145  tcrank  8962  rpnnen1lem5  12019  hashfun  13425  resqrex  14278  resqrtcl  14281  prmgaplem6  16041  lbsextlem3  19434  cmpsublem  21482  cmpcld  21485  ovoliunlem2  23561  isblo3i  28047  trisegint  32511  itg2addnclem  33816  areacirclem2  33856  lshpnelb  34872  lsatfixedN  34897  lsmsatcv  34898  lssatomic  34899  lcv1  34929  lsatcvatlem  34937  islshpcv  34941  lfl1  34958  lshpsmreu  34997  lshpkrex  35006  lshpset2N  35007  lkrlspeqN  35059  cvrval3  35301  1cvratlt  35362  ps-2b  35370  llnnleat  35401  lvolex3N  35426  lplncvrlvol2  35503  osumcllem7N  35850  lhp0lt  35891  lhpj1  35910  4atexlemex6  35962  4atexlem7  35963  trlnidat  36061  cdlemd9  36094  cdleme21h  36222  cdlemg7fvbwN  36495  cdlemg7aN  36513  cdlemg34  36600  cdlemg36  36602  cdlemg44  36621  cdlemg48  36625  tendo1ne0  36716  cdlemk26-3  36794  cdlemk55b  36848  cdleml4N  36867  dih1dimatlem0  37216  dihglblem6  37228  dochshpncl  37272  dvh4dimlem  37331  dvh3dim2  37336  dvh3dim3N  37337  dochsatshpb  37340  dochexmidlem4  37351  dochexmidlem5  37352  dochexmidlem8  37355  dochkr1  37366  dochkr1OLDN  37367  lcfl7lem  37387  lcfl6  37388  lcfl8  37390  lcfrlem16  37446  lcfrlem40  37470  mapdval2N  37518  mapdrvallem2  37533  mapdpglem24  37592  mapdh6iN  37632  mapdh8ad  37667  mapdh8e  37672  hdmap1l6i  37706  hdmapval0  37721  hdmapevec  37723  hdmapval3N  37726  hdmap10lem  37727  hdmap11lem2  37730  hdmaprnlem15N  37749  hdmaprnlem16N  37750  hdmap14lem10  37765  hdmap14lem11  37766  hdmap14lem12  37767  hdmap14lem14  37769  hgmapval0  37780  hgmapval1  37781  hgmapadd  37782  hgmapmul  37783  hgmaprnlem3N  37786  hgmaprnlem4N  37787  hgmap11  37790  hgmapvvlem3  37813  rpnnen3lem  38207  dvconstbi  39139  expgrowth  39140  eliuniin  39862  limccog  40422  0ellimcdiv  40451  cosknegpi  40650  cncfshift  40657  cncfperiod  40662  cncfuni  40669  icccncfext  40670  dvbdfbdioolem1  40713  itgperiod  40766  stoweidlem57  40843  fourierdlem12  40905  fourierdlem48  40940  fourierdlem49  40941  fourierdlem52  40944  fourierdlem54  40946  fourierdlem68  40960  fourierdlem77  40969  fourierdlem83  40975  fourierdlem87  40979  fourierdlem102  40994  fourierdlem103  40995  fourierdlem104  40996  fourierdlem113  41005  fourierdlem114  41006  elaa2  41020  etransclem24  41044  etransclem32  41052  etransclem48  41068  sigarcol  41625  f1oresf1o2  41972
  Copyright terms: Public domain W3C validator