Theorem rexlimdv3a 3033

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). Frequently-used variant of rexlimdv 3030. (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 1264	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	rexlimdv 3030	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∧ w3a 1037   ∈ wcel 1990  ∃wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  sorpssuni  6946  sorpssint  6947  tcrank  8747  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  hashfun  13224  resqrex  13991  resqrtcl  13994  prmgaplem6  15760  lbsextlem3  19160  cmpsublem  21202  cmpcld  21205  ovoliunlem2  23271  isblo3i  27656  trisegint  32135  itg2addnclem  33461  areacirclem2  33501  lshpnelb  34271  lsatfixedN  34296  lsmsatcv  34297  lssatomic  34298  lcv1  34328  lsatcvatlem  34336  islshpcv  34340  lfl1  34357  lshpsmreu  34396  lshpkrex  34405  lshpset2N  34406  lkrlspeqN  34458  cvrval3  34699  1cvratlt  34760  ps-2b  34768  llnnleat  34799  lvolex3N  34824  lplncvrlvol2  34901  osumcllem7N  35248  lhp0lt  35289  lhpj1  35308  4atexlemex6  35360  4atexlem7  35361  trlnidat  35460  cdlemd9  35493  cdleme21h  35622  cdlemg7fvbwN  35895  cdlemg7aN  35913  cdlemg34  36000  cdlemg36  36002  cdlemg44  36021  cdlemg48  36025  tendo1ne0  36116  cdlemk26-3  36194  cdlemk55b  36248  cdleml4N  36267  dih1dimatlem0  36617  dihglblem6  36629  dochshpncl  36673  dvh4dimlem  36732  dvh3dim2  36737  dvh3dim3N  36738  dochsatshpb  36741  dochexmidlem4  36752  dochexmidlem5  36753  dochexmidlem8  36756  dochkr1  36767  dochkr1OLDN  36768  lcfl7lem  36788  lcfl6  36789  lcfl8  36791  lcfrlem16  36847  lcfrlem40  36871  mapdval2N  36919  mapdrvallem2  36934  mapdpglem24  36993  mapdh6iN  37033  mapdh8ad  37068  mapdh8e  37073  hdmap1l6i  37108  hdmapval0  37125  hdmapevec  37127  hdmapval3N  37130  hdmap10lem  37131  hdmap11lem2  37134  hdmaprnlem15N  37153  hdmaprnlem16N  37154  hdmap14lem10  37169  hdmap14lem11  37170  hdmap14lem12  37171  hdmap14lem14  37173  hgmapval0  37184  hgmapval1  37185  hgmapadd  37186  hgmapmul  37187  hgmaprnlem3N  37190  hgmaprnlem4N  37191  hgmap11  37194  hgmapvvlem3  37217  rpnnen3lem  37598  dvconstbi  38533  expgrowth  38534  eliuniin  39279  limccog  39852  0ellimcdiv  39881  cosknegpi  40080  cncfshift  40087  cncfperiod  40092  cncfuni  40099  icccncfext  40100  dvbdfbdioolem1  40143  itgperiod  40197  stoweidlem57  40274  fourierdlem12  40336  fourierdlem48  40371  fourierdlem49  40372  fourierdlem52  40375  fourierdlem54  40377  fourierdlem68  40391  fourierdlem77  40400  fourierdlem83  40406  fourierdlem87  40410  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem113  40436  fourierdlem114  40437  elaa2  40451  etransclem24  40475  etransclem32  40483  etransclem48  40499  sigarcol  41053