Theorem rexlimdv3a 3170

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

Syntax hints:   → wi 4   ∧ w3a 1101   ∈ wcel 2145  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-ex 1803  df-rex 3090

This theorem is referenced by:  sorpssuni  7719  sorpssint  7720  mapsnd  8872  tcrank  9844  rpnnen1lem5  12996  hashfun  14464  resqrex  15291  resqrtcl  15294  fprodle  16040  prmgaplem6  17106  lbsextlem3  21253  cmpsublem  23517  cmpcld  23520  ovoliunlem2  25623  isblo3i  31062  trisegint  36391  itg2addnclem  38182  areacirclem2  38220  lshpnelb  39620  lsatfixedN  39645  lsmsatcv  39646  lssatomic  39647  lcv1  39677  lsatcvatlem  39685  islshpcv  39689  lfl1  39706  lshpsmreu  39745  lshpkrex  39754  lshpset2N  39755  lkrlspeqN  39807  cvrval3  40049  1cvratlt  40110  ps-2b  40118  llnnleat  40149  lvolex3N  40174  lplncvrlvol2  40251  osumcllem7N  40598  lhp0lt  40639  lhpj1  40658  4atexlemex6  40710  4atexlem7  40711  trlnidat  40809  cdlemd9  40842  cdleme21h  40970  cdlemg7fvbwN  41243  cdlemg7aN  41261  cdlemg34  41348  cdlemg36  41350  cdlemg44  41369  cdlemg48  41373  tendo1ne0  41464  cdlemk26-3  41542  cdlemk55b  41596  cdleml4N  41615  dih1dimatlem0  41964  dihglblem6  41976  dochshpncl  42020  dvh4dimlem  42079  dvh3dim2  42084  dvh3dim3N  42085  dochsatshpb  42088  dochexmidlem4  42099  dochexmidlem5  42100  dochexmidlem8  42103  dochkr1  42114  dochkr1OLDN  42115  lcfl7lem  42135  lcfl6  42136  lcfl8  42138  lcfrlem16  42194  lcfrlem40  42218  mapdval2N  42266  mapdrvallem2  42281  mapdpglem24  42340  mapdh6iN  42380  mapdh8ad  42415  mapdh8e  42420  hdmap1l6i  42454  hdmapval0  42469  hdmapevec  42471  hdmapval3N  42474  hdmap10lem  42475  hdmap11lem2  42478  hdmaprnlem15N  42497  hdmaprnlem16N  42498  hdmap14lem10  42513  hdmap14lem11  42514  hdmap14lem12  42515  hdmap14lem14  42517  hgmapval0  42528  hgmapval1  42529  hgmapadd  42530  hgmapmul  42531  hgmaprnlem3N  42534  hgmaprnlem4N  42535  hgmap11  42538  hgmapvvlem3  42561  rpnnen3lem  43620  onexlimgt  43832  grumnudlem  44859  dvconstbi  44908  expgrowth  44909  eliuniin  45675  wessf1ornlem  45761  ssmapsn  45790  limccog  46194  0ellimcdiv  46221  cosknegpi  46441  cncfshift  46446  cncfperiod  46451  cncfuni  46458  icccncfext  46459  dvbdfbdioolem1  46500  itgperiod  46553  stoweidlem57  46629  fourierdlem12  46691  fourierdlem48  46726  fourierdlem49  46727  fourierdlem52  46730  fourierdlem54  46732  fourierdlem68  46746  fourierdlem77  46755  fourierdlem83  46761  fourierdlem87  46765  fourierdlem102  46780  fourierdlem103  46781  fourierdlem104  46782  fourierdlem113  46791  fourierdlem114  46792  elaa2  46806  etransclem24  46830  etransclem32  46838  etransclem48  46854  ovolval5lem3  47226  sssmf  47310  sigarcol  47436  f1oresf1o2  47883  imaelsetpreimafv  47999  uhgrimisgrgriclem  48550