Theorem rexlimdv3a 3214

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

Syntax hints:   → wi 4   ∧ w3a 1085   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  sorpssuni  7563  sorpssint  7564  mapsnd  8632  tcrank  9573  rpnnen1lem5  12650  hashfun  14080  resqrex  14890  resqrtcl  14893  fprodle  15634  prmgaplem6  16685  lbsextlem3  20337  cmpsublem  22458  cmpcld  22461  ovoliunlem2  24572  isblo3i  29064  trisegint  34257  itg2addnclem  35755  areacirclem2  35793  lshpnelb  36925  lsatfixedN  36950  lsmsatcv  36951  lssatomic  36952  lcv1  36982  lsatcvatlem  36990  islshpcv  36994  lfl1  37011  lshpsmreu  37050  lshpkrex  37059  lshpset2N  37060  lkrlspeqN  37112  cvrval3  37354  1cvratlt  37415  ps-2b  37423  llnnleat  37454  lvolex3N  37479  lplncvrlvol2  37556  osumcllem7N  37903  lhp0lt  37944  lhpj1  37963  4atexlemex6  38015  4atexlem7  38016  trlnidat  38114  cdlemd9  38147  cdleme21h  38275  cdlemg7fvbwN  38548  cdlemg7aN  38566  cdlemg34  38653  cdlemg36  38655  cdlemg44  38674  cdlemg48  38678  tendo1ne0  38769  cdlemk26-3  38847  cdlemk55b  38901  cdleml4N  38920  dih1dimatlem0  39269  dihglblem6  39281  dochshpncl  39325  dvh4dimlem  39384  dvh3dim2  39389  dvh3dim3N  39390  dochsatshpb  39393  dochexmidlem4  39404  dochexmidlem5  39405  dochexmidlem8  39408  dochkr1  39419  dochkr1OLDN  39420  lcfl7lem  39440  lcfl6  39441  lcfl8  39443  lcfrlem16  39499  lcfrlem40  39523  mapdval2N  39571  mapdrvallem2  39586  mapdpglem24  39645  mapdh6iN  39685  mapdh8ad  39720  mapdh8e  39725  hdmap1l6i  39759  hdmapval0  39774  hdmapevec  39776  hdmapval3N  39779  hdmap10lem  39780  hdmap11lem2  39783  hdmaprnlem15N  39802  hdmaprnlem16N  39803  hdmap14lem10  39818  hdmap14lem11  39819  hdmap14lem12  39820  hdmap14lem14  39822  hgmapval0  39833  hgmapval1  39834  hgmapadd  39835  hgmapmul  39836  hgmaprnlem3N  39839  hgmaprnlem4N  39840  hgmap11  39843  hgmapvvlem3  39866  rpnnen3lem  40769  grumnudlem  41792  dvconstbi  41841  expgrowth  41842  eliuniin  42538  wessf1ornlem  42611  limccog  43051  0ellimcdiv  43080  cosknegpi  43300  cncfshift  43305  cncfperiod  43310  cncfuni  43317  icccncfext  43318  dvbdfbdioolem1  43359  itgperiod  43412  stoweidlem57  43488  fourierdlem12  43550  fourierdlem48  43585  fourierdlem49  43586  fourierdlem52  43589  fourierdlem54  43591  fourierdlem68  43605  fourierdlem77  43614  fourierdlem83  43620  fourierdlem87  43624  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem113  43650  fourierdlem114  43651  elaa2  43665  etransclem24  43689  etransclem32  43697  etransclem48  43713  sigarcol  44267  f1oresf1o2  44670  imaelsetpreimafv  44735