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

Theorem rexlimdv3a 3215
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 3212. (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 1121 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32rexlimdv 3212 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1089  wcel 2112  wrex 3065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1091  df-ex 1788  df-ral 3069  df-rex 3070
This theorem is referenced by:  sorpssuni  7542  sorpssint  7543  mapsnd  8591  tcrank  9530  rpnnen1lem5  12607  hashfun  14037  resqrex  14847  resqrtcl  14850  fprodle  15591  prmgaplem6  16642  lbsextlem3  20230  cmpsublem  22328  cmpcld  22331  ovoliunlem2  24432  isblo3i  28914  trisegint  34101  itg2addnclem  35602  areacirclem2  35640  lshpnelb  36772  lsatfixedN  36797  lsmsatcv  36798  lssatomic  36799  lcv1  36829  lsatcvatlem  36837  islshpcv  36841  lfl1  36858  lshpsmreu  36897  lshpkrex  36906  lshpset2N  36907  lkrlspeqN  36959  cvrval3  37201  1cvratlt  37262  ps-2b  37270  llnnleat  37301  lvolex3N  37326  lplncvrlvol2  37403  osumcllem7N  37750  lhp0lt  37791  lhpj1  37810  4atexlemex6  37862  4atexlem7  37863  trlnidat  37961  cdlemd9  37994  cdleme21h  38122  cdlemg7fvbwN  38395  cdlemg7aN  38413  cdlemg34  38500  cdlemg36  38502  cdlemg44  38521  cdlemg48  38525  tendo1ne0  38616  cdlemk26-3  38694  cdlemk55b  38748  cdleml4N  38767  dih1dimatlem0  39116  dihglblem6  39128  dochshpncl  39172  dvh4dimlem  39231  dvh3dim2  39236  dvh3dim3N  39237  dochsatshpb  39240  dochexmidlem4  39251  dochexmidlem5  39252  dochexmidlem8  39255  dochkr1  39266  dochkr1OLDN  39267  lcfl7lem  39287  lcfl6  39288  lcfl8  39290  lcfrlem16  39346  lcfrlem40  39370  mapdval2N  39418  mapdrvallem2  39433  mapdpglem24  39492  mapdh6iN  39532  mapdh8ad  39567  mapdh8e  39572  hdmap1l6i  39606  hdmapval0  39621  hdmapevec  39623  hdmapval3N  39626  hdmap10lem  39627  hdmap11lem2  39630  hdmaprnlem15N  39649  hdmaprnlem16N  39650  hdmap14lem10  39665  hdmap14lem11  39666  hdmap14lem12  39667  hdmap14lem14  39669  hgmapval0  39680  hgmapval1  39681  hgmapadd  39682  hgmapmul  39683  hgmaprnlem3N  39686  hgmaprnlem4N  39687  hgmap11  39690  hgmapvvlem3  39713  rpnnen3lem  40604  grumnudlem  41624  dvconstbi  41673  expgrowth  41674  eliuniin  42370  wessf1ornlem  42443  limccog  42882  0ellimcdiv  42911  cosknegpi  43131  cncfshift  43136  cncfperiod  43141  cncfuni  43148  icccncfext  43149  dvbdfbdioolem1  43190  itgperiod  43243  stoweidlem57  43319  fourierdlem12  43381  fourierdlem48  43416  fourierdlem49  43417  fourierdlem52  43420  fourierdlem54  43422  fourierdlem68  43436  fourierdlem77  43445  fourierdlem83  43451  fourierdlem87  43455  fourierdlem102  43470  fourierdlem103  43471  fourierdlem104  43472  fourierdlem113  43481  fourierdlem114  43482  elaa2  43496  etransclem24  43520  etransclem32  43528  etransclem48  43544  sigarcol  44098  f1oresf1o2  44501  imaelsetpreimafv  44566
  Copyright terms: Public domain W3C validator