Theorem rexlimdv3a 3288

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

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

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 3145  df-rex 3146

This theorem is referenced by:  sorpssuni  7460  sorpssint  7461  mapsnd  8452  tcrank  9315  rpnnen1lem5  12383  hashfun  13801  resqrex  14612  resqrtcl  14615  fprodle  15352  prmgaplem6  16394  lbsextlem3  19934  cmpsublem  22009  cmpcld  22012  ovoliunlem2  24106  isblo3i  28580  trisegint  33491  itg2addnclem  34945  areacirclem2  34985  lshpnelb  36122  lsatfixedN  36147  lsmsatcv  36148  lssatomic  36149  lcv1  36179  lsatcvatlem  36187  islshpcv  36191  lfl1  36208  lshpsmreu  36247  lshpkrex  36256  lshpset2N  36257  lkrlspeqN  36309  cvrval3  36551  1cvratlt  36612  ps-2b  36620  llnnleat  36651  lvolex3N  36676  lplncvrlvol2  36753  osumcllem7N  37100  lhp0lt  37141  lhpj1  37160  4atexlemex6  37212  4atexlem7  37213  trlnidat  37311  cdlemd9  37344  cdleme21h  37472  cdlemg7fvbwN  37745  cdlemg7aN  37763  cdlemg34  37850  cdlemg36  37852  cdlemg44  37871  cdlemg48  37875  tendo1ne0  37966  cdlemk26-3  38044  cdlemk55b  38098  cdleml4N  38117  dih1dimatlem0  38466  dihglblem6  38478  dochshpncl  38522  dvh4dimlem  38581  dvh3dim2  38586  dvh3dim3N  38587  dochsatshpb  38590  dochexmidlem4  38601  dochexmidlem5  38602  dochexmidlem8  38605  dochkr1  38616  dochkr1OLDN  38617  lcfl7lem  38637  lcfl6  38638  lcfl8  38640  lcfrlem16  38696  lcfrlem40  38720  mapdval2N  38768  mapdrvallem2  38783  mapdpglem24  38842  mapdh6iN  38882  mapdh8ad  38917  mapdh8e  38922  hdmap1l6i  38956  hdmapval0  38971  hdmapevec  38973  hdmapval3N  38976  hdmap10lem  38977  hdmap11lem2  38980  hdmaprnlem15N  38999  hdmaprnlem16N  39000  hdmap14lem10  39015  hdmap14lem11  39016  hdmap14lem12  39017  hdmap14lem14  39019  hgmapval0  39030  hgmapval1  39031  hgmapadd  39032  hgmapmul  39033  hgmaprnlem3N  39036  hgmaprnlem4N  39037  hgmap11  39040  hgmapvvlem3  39063  rpnnen3lem  39635  grumnudlem  40628  dvconstbi  40673  expgrowth  40674  eliuniin  41372  wessf1ornlem  41452  limccog  41908  0ellimcdiv  41937  cosknegpi  42157  cncfshift  42164  cncfperiod  42169  cncfuni  42176  icccncfext  42177  dvbdfbdioolem1  42220  itgperiod  42273  stoweidlem57  42349  fourierdlem12  42411  fourierdlem48  42446  fourierdlem49  42447  fourierdlem52  42450  fourierdlem54  42452  fourierdlem68  42466  fourierdlem77  42475  fourierdlem83  42481  fourierdlem87  42485  fourierdlem102  42500  fourierdlem103  42501  fourierdlem104  42502  fourierdlem113  42511  fourierdlem114  42512  elaa2  42526  etransclem24  42550  etransclem32  42558  etransclem48  42574  sigarcol  43128  f1oresf1o2  43497  imaelsetpreimafv  43562