Theorem rexlimdv3a 3151

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

Syntax hints:   → wi 4   ∧ w3a 1084   ∈ wcel 2098  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1086  df-ex 1774  df-rex 3063

This theorem is referenced by:  sorpssuni  7716  sorpssint  7717  mapsnd  8877  tcrank  9876  rpnnen1lem5  12963  hashfun  14395  resqrex  15195  resqrtcl  15198  fprodle  15938  prmgaplem6  16990  lbsextlem3  21003  cmpsublem  23227  cmpcld  23230  ovoliunlem2  25356  isblo3i  30526  trisegint  35496  itg2addnclem  37033  areacirclem2  37071  lshpnelb  38348  lsatfixedN  38373  lsmsatcv  38374  lssatomic  38375  lcv1  38405  lsatcvatlem  38413  islshpcv  38417  lfl1  38434  lshpsmreu  38473  lshpkrex  38482  lshpset2N  38483  lkrlspeqN  38535  cvrval3  38778  1cvratlt  38839  ps-2b  38847  llnnleat  38878  lvolex3N  38903  lplncvrlvol2  38980  osumcllem7N  39327  lhp0lt  39368  lhpj1  39387  4atexlemex6  39439  4atexlem7  39440  trlnidat  39538  cdlemd9  39571  cdleme21h  39699  cdlemg7fvbwN  39972  cdlemg7aN  39990  cdlemg34  40077  cdlemg36  40079  cdlemg44  40098  cdlemg48  40102  tendo1ne0  40193  cdlemk26-3  40271  cdlemk55b  40325  cdleml4N  40344  dih1dimatlem0  40693  dihglblem6  40705  dochshpncl  40749  dvh4dimlem  40808  dvh3dim2  40813  dvh3dim3N  40814  dochsatshpb  40817  dochexmidlem4  40828  dochexmidlem5  40829  dochexmidlem8  40832  dochkr1  40843  dochkr1OLDN  40844  lcfl7lem  40864  lcfl6  40865  lcfl8  40867  lcfrlem16  40923  lcfrlem40  40947  mapdval2N  40995  mapdrvallem2  41010  mapdpglem24  41069  mapdh6iN  41109  mapdh8ad  41144  mapdh8e  41149  hdmap1l6i  41183  hdmapval0  41198  hdmapevec  41200  hdmapval3N  41203  hdmap10lem  41204  hdmap11lem2  41207  hdmaprnlem15N  41226  hdmaprnlem16N  41227  hdmap14lem10  41242  hdmap14lem11  41243  hdmap14lem12  41244  hdmap14lem14  41246  hgmapval0  41257  hgmapval1  41258  hgmapadd  41259  hgmapmul  41260  hgmaprnlem3N  41263  hgmaprnlem4N  41264  hgmap11  41267  hgmapvvlem3  41290  rpnnen3lem  42284  onexlimgt  42506  grumnudlem  43558  dvconstbi  43607  expgrowth  43608  eliuniin  44301  wessf1ornlem  44394  limccog  44846  0ellimcdiv  44875  cosknegpi  45095  cncfshift  45100  cncfperiod  45105  cncfuni  45112  icccncfext  45113  dvbdfbdioolem1  45154  itgperiod  45207  stoweidlem57  45283  fourierdlem12  45345  fourierdlem48  45380  fourierdlem49  45381  fourierdlem52  45384  fourierdlem54  45386  fourierdlem68  45400  fourierdlem77  45409  fourierdlem83  45415  fourierdlem87  45419  fourierdlem102  45434  fourierdlem103  45435  fourierdlem104  45436  fourierdlem113  45445  fourierdlem114  45446  elaa2  45460  etransclem24  45484  etransclem32  45492  etransclem48  45508  ovolval5lem3  45880  sigarcol  46090  f1oresf1o2  46509  imaelsetpreimafv  46573