Theorem rexlimdv3a 3286

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

Syntax hints:   → wi 4   ∧ w3a 1083   ∈ wcel 2114  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085  df-ex 1781  df-ral 3143  df-rex 3144

This theorem is referenced by:  sorpssuni  7444  sorpssint  7445  mapsnd  8436  tcrank  9299  rpnnen1lem5  12367  hashfun  13788  resqrex  14595  resqrtcl  14598  fprodle  15335  prmgaplem6  16375  lbsextlem3  19915  cmpsublem  21990  cmpcld  21993  ovoliunlem2  24087  isblo3i  28562  trisegint  33496  itg2addnclem  34977  areacirclem2  35015  lshpnelb  36152  lsatfixedN  36177  lsmsatcv  36178  lssatomic  36179  lcv1  36209  lsatcvatlem  36217  islshpcv  36221  lfl1  36238  lshpsmreu  36277  lshpkrex  36286  lshpset2N  36287  lkrlspeqN  36339  cvrval3  36581  1cvratlt  36642  ps-2b  36650  llnnleat  36681  lvolex3N  36706  lplncvrlvol2  36783  osumcllem7N  37130  lhp0lt  37171  lhpj1  37190  4atexlemex6  37242  4atexlem7  37243  trlnidat  37341  cdlemd9  37374  cdleme21h  37502  cdlemg7fvbwN  37775  cdlemg7aN  37793  cdlemg34  37880  cdlemg36  37882  cdlemg44  37901  cdlemg48  37905  tendo1ne0  37996  cdlemk26-3  38074  cdlemk55b  38128  cdleml4N  38147  dih1dimatlem0  38496  dihglblem6  38508  dochshpncl  38552  dvh4dimlem  38611  dvh3dim2  38616  dvh3dim3N  38617  dochsatshpb  38620  dochexmidlem4  38631  dochexmidlem5  38632  dochexmidlem8  38635  dochkr1  38646  dochkr1OLDN  38647  lcfl7lem  38667  lcfl6  38668  lcfl8  38670  lcfrlem16  38726  lcfrlem40  38750  mapdval2N  38798  mapdrvallem2  38813  mapdpglem24  38872  mapdh6iN  38912  mapdh8ad  38947  mapdh8e  38952  hdmap1l6i  38986  hdmapval0  39001  hdmapevec  39003  hdmapval3N  39006  hdmap10lem  39007  hdmap11lem2  39010  hdmaprnlem15N  39029  hdmaprnlem16N  39030  hdmap14lem10  39045  hdmap14lem11  39046  hdmap14lem12  39047  hdmap14lem14  39049  hgmapval0  39060  hgmapval1  39061  hgmapadd  39062  hgmapmul  39063  hgmaprnlem3N  39066  hgmaprnlem4N  39067  hgmap11  39070  hgmapvvlem3  39093  rpnnen3lem  39720  grumnudlem  40711  dvconstbi  40756  expgrowth  40757  eliuniin  41455  wessf1ornlem  41535  limccog  41991  0ellimcdiv  42020  cosknegpi  42240  cncfshift  42247  cncfperiod  42252  cncfuni  42259  icccncfext  42260  dvbdfbdioolem1  42303  itgperiod  42356  stoweidlem57  42432  fourierdlem12  42494  fourierdlem48  42529  fourierdlem49  42530  fourierdlem52  42533  fourierdlem54  42535  fourierdlem68  42549  fourierdlem77  42558  fourierdlem83  42564  fourierdlem87  42568  fourierdlem102  42583  fourierdlem103  42584  fourierdlem104  42585  fourierdlem113  42594  fourierdlem114  42595  elaa2  42609  etransclem24  42633  etransclem32  42641  etransclem48  42657  sigarcol  43211  f1oresf1o2  43580  imaelsetpreimafv  43645