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

Theorem rexlimdv3a 3062
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 3059. (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 1283 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32rexlimdv 3059 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1054  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1056  df-ex 1745  df-ral 2946  df-rex 2947
This theorem is referenced by:  sorpssuni  6988  sorpssint  6989  tcrank  8785  rpnnen1lem5  11856  rpnnen1lem5OLD  11862  hashfun  13262  resqrex  14035  resqrtcl  14038  prmgaplem6  15807  lbsextlem3  19208  cmpsublem  21250  cmpcld  21253  ovoliunlem2  23317  isblo3i  27784  trisegint  32260  itg2addnclem  33591  areacirclem2  33631  lshpnelb  34589  lsatfixedN  34614  lsmsatcv  34615  lssatomic  34616  lcv1  34646  lsatcvatlem  34654  islshpcv  34658  lfl1  34675  lshpsmreu  34714  lshpkrex  34723  lshpset2N  34724  lkrlspeqN  34776  cvrval3  35017  1cvratlt  35078  ps-2b  35086  llnnleat  35117  lvolex3N  35142  lplncvrlvol2  35219  osumcllem7N  35566  lhp0lt  35607  lhpj1  35626  4atexlemex6  35678  4atexlem7  35679  trlnidat  35778  cdlemd9  35811  cdleme21h  35939  cdlemg7fvbwN  36212  cdlemg7aN  36230  cdlemg34  36317  cdlemg36  36319  cdlemg44  36338  cdlemg48  36342  tendo1ne0  36433  cdlemk26-3  36511  cdlemk55b  36565  cdleml4N  36584  dih1dimatlem0  36934  dihglblem6  36946  dochshpncl  36990  dvh4dimlem  37049  dvh3dim2  37054  dvh3dim3N  37055  dochsatshpb  37058  dochexmidlem4  37069  dochexmidlem5  37070  dochexmidlem8  37073  dochkr1  37084  dochkr1OLDN  37085  lcfl7lem  37105  lcfl6  37106  lcfl8  37108  lcfrlem16  37164  lcfrlem40  37188  mapdval2N  37236  mapdrvallem2  37251  mapdpglem24  37310  mapdh6iN  37350  mapdh8ad  37385  mapdh8e  37390  hdmap1l6i  37425  hdmapval0  37442  hdmapevec  37444  hdmapval3N  37447  hdmap10lem  37448  hdmap11lem2  37451  hdmaprnlem15N  37470  hdmaprnlem16N  37471  hdmap14lem10  37486  hdmap14lem11  37487  hdmap14lem12  37488  hdmap14lem14  37490  hgmapval0  37501  hgmapval1  37502  hgmapadd  37503  hgmapmul  37504  hgmaprnlem3N  37507  hgmaprnlem4N  37508  hgmap11  37511  hgmapvvlem3  37534  rpnnen3lem  37915  dvconstbi  38850  expgrowth  38851  eliuniin  39593  limccog  40170  0ellimcdiv  40199  cosknegpi  40398  cncfshift  40405  cncfperiod  40410  cncfuni  40417  icccncfext  40418  dvbdfbdioolem1  40461  itgperiod  40515  stoweidlem57  40592  fourierdlem12  40654  fourierdlem48  40689  fourierdlem49  40690  fourierdlem52  40693  fourierdlem54  40695  fourierdlem68  40709  fourierdlem77  40718  fourierdlem83  40724  fourierdlem87  40728  fourierdlem102  40743  fourierdlem103  40744  fourierdlem104  40745  fourierdlem113  40754  fourierdlem114  40755  elaa2  40769  etransclem24  40793  etransclem32  40801  etransclem48  40817  sigarcol  41374
  Copyright terms: Public domain W3C validator