Theorem rexlimdv3a 3166

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

Syntax hints:   → wi 4   ∧ w3a 1097   ∈ wcel 2141  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1099  df-ex 1799  df-rex 3086

This theorem is referenced by:  sorpssuni  7711  sorpssint  7712  mapsnd  8864  tcrank  9839  rpnnen1lem5  12979  hashfun  14447  resqrex  15260  resqrtcl  15263  fprodle  16009  prmgaplem6  17075  lbsextlem3  21210  cmpsublem  23439  cmpcld  23442  ovoliunlem2  25545  isblo3i  30950  trisegint  36342  itg2addnclem  38134  areacirclem2  38172  lshpnelb  39572  lsatfixedN  39597  lsmsatcv  39598  lssatomic  39599  lcv1  39629  lsatcvatlem  39637  islshpcv  39641  lfl1  39658  lshpsmreu  39697  lshpkrex  39706  lshpset2N  39707  lkrlspeqN  39759  cvrval3  40001  1cvratlt  40062  ps-2b  40070  llnnleat  40101  lvolex3N  40126  lplncvrlvol2  40203  osumcllem7N  40550  lhp0lt  40591  lhpj1  40610  4atexlemex6  40662  4atexlem7  40663  trlnidat  40761  cdlemd9  40794  cdleme21h  40922  cdlemg7fvbwN  41195  cdlemg7aN  41213  cdlemg34  41300  cdlemg36  41302  cdlemg44  41321  cdlemg48  41325  tendo1ne0  41416  cdlemk26-3  41494  cdlemk55b  41548  cdleml4N  41567  dih1dimatlem0  41916  dihglblem6  41928  dochshpncl  41972  dvh4dimlem  42031  dvh3dim2  42036  dvh3dim3N  42037  dochsatshpb  42040  dochexmidlem4  42051  dochexmidlem5  42052  dochexmidlem8  42055  dochkr1  42066  dochkr1OLDN  42067  lcfl7lem  42087  lcfl6  42088  lcfl8  42090  lcfrlem16  42146  lcfrlem40  42170  mapdval2N  42218  mapdrvallem2  42233  mapdpglem24  42292  mapdh6iN  42332  mapdh8ad  42367  mapdh8e  42372  hdmap1l6i  42406  hdmapval0  42421  hdmapevec  42423  hdmapval3N  42426  hdmap10lem  42427  hdmap11lem2  42430  hdmaprnlem15N  42449  hdmaprnlem16N  42450  hdmap14lem10  42465  hdmap14lem11  42466  hdmap14lem12  42467  hdmap14lem14  42469  hgmapval0  42480  hgmapval1  42481  hgmapadd  42482  hgmapmul  42483  hgmaprnlem3N  42486  hgmaprnlem4N  42487  hgmap11  42490  hgmapvvlem3  42513  rpnnen3lem  43572  onexlimgt  43784  grumnudlem  44825  dvconstbi  44874  expgrowth  44875  eliuniin  45641  wessf1ornlem  45727  ssmapsn  45756  limccog  46160  0ellimcdiv  46187  cosknegpi  46407  cncfshift  46412  cncfperiod  46417  cncfuni  46424  icccncfext  46425  dvbdfbdioolem1  46466  itgperiod  46519  stoweidlem57  46595  fourierdlem12  46657  fourierdlem48  46692  fourierdlem49  46693  fourierdlem52  46696  fourierdlem54  46698  fourierdlem68  46712  fourierdlem77  46721  fourierdlem83  46727  fourierdlem87  46731  fourierdlem102  46746  fourierdlem103  46747  fourierdlem104  46748  fourierdlem113  46757  fourierdlem114  46758  elaa2  46772  etransclem24  46796  etransclem32  46804  etransclem48  46820  ovolval5lem3  47192  sssmf  47276  sigarcol  47402  f1oresf1o2  47849  imaelsetpreimafv  47965  uhgrimisgrgriclem  48516