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

Theorem rexlimdv3a 3181
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 3178. (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 1112 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32rexlimdv 3178 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1071  wcel 2145  wrex 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991
This theorem depends on definitions:  df-bi 197  df-an 383  df-3an 1073  df-ex 1853  df-ral 3066  df-rex 3067
This theorem is referenced by:  sorpssuni  7093  sorpssint  7094  tcrank  8911  rpnnen1lem5  12021  rpnnen1lem5OLD  12027  hashfun  13426  resqrex  14199  resqrtcl  14202  prmgaplem6  15967  lbsextlem3  19375  cmpsublem  21423  cmpcld  21426  ovoliunlem2  23491  isblo3i  27996  trisegint  32472  itg2addnclem  33793  areacirclem2  33833  lshpnelb  34793  lsatfixedN  34818  lsmsatcv  34819  lssatomic  34820  lcv1  34850  lsatcvatlem  34858  islshpcv  34862  lfl1  34879  lshpsmreu  34918  lshpkrex  34927  lshpset2N  34928  lkrlspeqN  34980  cvrval3  35221  1cvratlt  35282  ps-2b  35290  llnnleat  35321  lvolex3N  35346  lplncvrlvol2  35423  osumcllem7N  35770  lhp0lt  35811  lhpj1  35830  4atexlemex6  35882  4atexlem7  35883  trlnidat  35982  cdlemd9  36015  cdleme21h  36143  cdlemg7fvbwN  36416  cdlemg7aN  36434  cdlemg34  36521  cdlemg36  36523  cdlemg44  36542  cdlemg48  36546  tendo1ne0  36637  cdlemk26-3  36715  cdlemk55b  36769  cdleml4N  36788  dih1dimatlem0  37138  dihglblem6  37150  dochshpncl  37194  dvh4dimlem  37253  dvh3dim2  37258  dvh3dim3N  37259  dochsatshpb  37262  dochexmidlem4  37273  dochexmidlem5  37274  dochexmidlem8  37277  dochkr1  37288  dochkr1OLDN  37289  lcfl7lem  37309  lcfl6  37310  lcfl8  37312  lcfrlem16  37368  lcfrlem40  37392  mapdval2N  37440  mapdrvallem2  37455  mapdpglem24  37514  mapdh6iN  37554  mapdh8ad  37589  mapdh8e  37594  hdmap1l6i  37628  hdmapval0  37643  hdmapevec  37645  hdmapval3N  37648  hdmap10lem  37649  hdmap11lem2  37652  hdmaprnlem15N  37671  hdmaprnlem16N  37672  hdmap14lem10  37687  hdmap14lem11  37688  hdmap14lem12  37689  hdmap14lem14  37691  hgmapval0  37702  hgmapval1  37703  hgmapadd  37704  hgmapmul  37705  hgmaprnlem3N  37708  hgmaprnlem4N  37709  hgmap11  37712  hgmapvvlem3  37735  rpnnen3lem  38124  dvconstbi  39059  expgrowth  39060  eliuniin  39800  limccog  40370  0ellimcdiv  40399  cosknegpi  40598  cncfshift  40605  cncfperiod  40610  cncfuni  40617  icccncfext  40618  dvbdfbdioolem1  40661  itgperiod  40714  stoweidlem57  40791  fourierdlem12  40853  fourierdlem48  40888  fourierdlem49  40889  fourierdlem52  40892  fourierdlem54  40894  fourierdlem68  40908  fourierdlem77  40917  fourierdlem83  40923  fourierdlem87  40927  fourierdlem102  40942  fourierdlem103  40943  fourierdlem104  40944  fourierdlem113  40953  fourierdlem114  40954  elaa2  40968  etransclem24  40992  etransclem32  41000  etransclem48  41016  sigarcol  41573  f1oresf1o2  41833
  Copyright terms: Public domain W3C validator