Theorem rexlimdv3a 3139

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 3133. (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

Step	Hyp	Ref	Expression
1		rexlimdv3a.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜓) → 𝜒)
2	1	3exp 1119	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	rexlimdv 3133	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2109  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-rex 3055

This theorem is referenced by:  sorpssuni  7711  sorpssint  7712  mapsnd  8862  tcrank  9844  rpnnen1lem5  12947  hashfun  14409  resqrex  15223  resqrtcl  15226  fprodle  15969  prmgaplem6  17034  lbsextlem3  21077  cmpsublem  23293  cmpcld  23296  ovoliunlem2  25411  isblo3i  30737  trisegint  36023  itg2addnclem  37672  areacirclem2  37710  lshpnelb  38984  lsatfixedN  39009  lsmsatcv  39010  lssatomic  39011  lcv1  39041  lsatcvatlem  39049  islshpcv  39053  lfl1  39070  lshpsmreu  39109  lshpkrex  39118  lshpset2N  39119  lkrlspeqN  39171  cvrval3  39414  1cvratlt  39475  ps-2b  39483  llnnleat  39514  lvolex3N  39539  lplncvrlvol2  39616  osumcllem7N  39963  lhp0lt  40004  lhpj1  40023  4atexlemex6  40075  4atexlem7  40076  trlnidat  40174  cdlemd9  40207  cdleme21h  40335  cdlemg7fvbwN  40608  cdlemg7aN  40626  cdlemg34  40713  cdlemg36  40715  cdlemg44  40734  cdlemg48  40738  tendo1ne0  40829  cdlemk26-3  40907  cdlemk55b  40961  cdleml4N  40980  dih1dimatlem0  41329  dihglblem6  41341  dochshpncl  41385  dvh4dimlem  41444  dvh3dim2  41449  dvh3dim3N  41450  dochsatshpb  41453  dochexmidlem4  41464  dochexmidlem5  41465  dochexmidlem8  41468  dochkr1  41479  dochkr1OLDN  41480  lcfl7lem  41500  lcfl6  41501  lcfl8  41503  lcfrlem16  41559  lcfrlem40  41583  mapdval2N  41631  mapdrvallem2  41646  mapdpglem24  41705  mapdh6iN  41745  mapdh8ad  41780  mapdh8e  41785  hdmap1l6i  41819  hdmapval0  41834  hdmapevec  41836  hdmapval3N  41839  hdmap10lem  41840  hdmap11lem2  41843  hdmaprnlem15N  41862  hdmaprnlem16N  41863  hdmap14lem10  41878  hdmap14lem11  41879  hdmap14lem12  41880  hdmap14lem14  41882  hgmapval0  41893  hgmapval1  41894  hgmapadd  41895  hgmapmul  41896  hgmaprnlem3N  41899  hgmaprnlem4N  41900  hgmap11  41903  hgmapvvlem3  41926  rpnnen3lem  43027  onexlimgt  43239  grumnudlem  44281  dvconstbi  44330  expgrowth  44331  eliuniin  45100  wessf1ornlem  45186  ssmapsn  45217  limccog  45625  0ellimcdiv  45654  cosknegpi  45874  cncfshift  45879  cncfperiod  45884  cncfuni  45891  icccncfext  45892  dvbdfbdioolem1  45933  itgperiod  45986  stoweidlem57  46062  fourierdlem12  46124  fourierdlem48  46159  fourierdlem49  46160  fourierdlem52  46163  fourierdlem54  46165  fourierdlem68  46179  fourierdlem77  46188  fourierdlem83  46194  fourierdlem87  46198  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem113  46224  fourierdlem114  46225  elaa2  46239  etransclem24  46263  etransclem32  46271  etransclem48  46287  ovolval5lem3  46659  sigarcol  46869  f1oresf1o2  47296  imaelsetpreimafv  47400  uhgrimisgrgriclem  47934