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

Theorem rexlimdv3a 3248
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 3245. (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 1116 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32rexlimdv 3245 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084  wcel 2112  wrex 3110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-ral 3114  df-rex 3115
This theorem is referenced by:  sorpssuni  7442  sorpssint  7443  mapsnd  8437  tcrank  9301  rpnnen1lem5  12372  hashfun  13798  resqrex  14605  resqrtcl  14608  fprodle  15345  prmgaplem6  16385  lbsextlem3  19928  cmpsublem  22007  cmpcld  22010  ovoliunlem2  24110  isblo3i  28587  trisegint  33597  itg2addnclem  35101  areacirclem2  35139  lshpnelb  36273  lsatfixedN  36298  lsmsatcv  36299  lssatomic  36300  lcv1  36330  lsatcvatlem  36338  islshpcv  36342  lfl1  36359  lshpsmreu  36398  lshpkrex  36407  lshpset2N  36408  lkrlspeqN  36460  cvrval3  36702  1cvratlt  36763  ps-2b  36771  llnnleat  36802  lvolex3N  36827  lplncvrlvol2  36904  osumcllem7N  37251  lhp0lt  37292  lhpj1  37311  4atexlemex6  37363  4atexlem7  37364  trlnidat  37462  cdlemd9  37495  cdleme21h  37623  cdlemg7fvbwN  37896  cdlemg7aN  37914  cdlemg34  38001  cdlemg36  38003  cdlemg44  38022  cdlemg48  38026  tendo1ne0  38117  cdlemk26-3  38195  cdlemk55b  38249  cdleml4N  38268  dih1dimatlem0  38617  dihglblem6  38629  dochshpncl  38673  dvh4dimlem  38732  dvh3dim2  38737  dvh3dim3N  38738  dochsatshpb  38741  dochexmidlem4  38752  dochexmidlem5  38753  dochexmidlem8  38756  dochkr1  38767  dochkr1OLDN  38768  lcfl7lem  38788  lcfl6  38789  lcfl8  38791  lcfrlem16  38847  lcfrlem40  38871  mapdval2N  38919  mapdrvallem2  38934  mapdpglem24  38993  mapdh6iN  39033  mapdh8ad  39068  mapdh8e  39073  hdmap1l6i  39107  hdmapval0  39122  hdmapevec  39124  hdmapval3N  39127  hdmap10lem  39128  hdmap11lem2  39131  hdmaprnlem15N  39150  hdmaprnlem16N  39151  hdmap14lem10  39166  hdmap14lem11  39167  hdmap14lem12  39168  hdmap14lem14  39170  hgmapval0  39181  hgmapval1  39182  hgmapadd  39183  hgmapmul  39184  hgmaprnlem3N  39187  hgmaprnlem4N  39188  hgmap11  39191  hgmapvvlem3  39214  rpnnen3lem  39959  grumnudlem  40980  dvconstbi  41025  expgrowth  41026  eliuniin  41722  wessf1ornlem  41798  limccog  42249  0ellimcdiv  42278  cosknegpi  42498  cncfshift  42503  cncfperiod  42508  cncfuni  42515  icccncfext  42516  dvbdfbdioolem1  42557  itgperiod  42610  stoweidlem57  42686  fourierdlem12  42748  fourierdlem48  42783  fourierdlem49  42784  fourierdlem52  42787  fourierdlem54  42789  fourierdlem68  42803  fourierdlem77  42812  fourierdlem83  42818  fourierdlem87  42822  fourierdlem102  42837  fourierdlem103  42838  fourierdlem104  42839  fourierdlem113  42848  fourierdlem114  42849  elaa2  42863  etransclem24  42887  etransclem32  42895  etransclem48  42911  sigarcol  43465  f1oresf1o2  43834  imaelsetpreimafv  43899
  Copyright terms: Public domain W3C validator