Theorem rexlimdv3a 3159

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

Syntax hints:   → wi 4   ∧ w3a 1087   ∈ wcel 2106  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1089  df-ex 1782  df-rex 3071

This theorem is referenced by:  sorpssuni  7724  sorpssint  7725  mapsnd  8882  tcrank  9881  rpnnen1lem5  12967  hashfun  14399  resqrex  15199  resqrtcl  15202  fprodle  15942  prmgaplem6  16991  lbsextlem3  20779  cmpsublem  22910  cmpcld  22913  ovoliunlem2  25027  isblo3i  30092  trisegint  35069  itg2addnclem  36625  areacirclem2  36663  lshpnelb  37940  lsatfixedN  37965  lsmsatcv  37966  lssatomic  37967  lcv1  37997  lsatcvatlem  38005  islshpcv  38009  lfl1  38026  lshpsmreu  38065  lshpkrex  38074  lshpset2N  38075  lkrlspeqN  38127  cvrval3  38370  1cvratlt  38431  ps-2b  38439  llnnleat  38470  lvolex3N  38495  lplncvrlvol2  38572  osumcllem7N  38919  lhp0lt  38960  lhpj1  38979  4atexlemex6  39031  4atexlem7  39032  trlnidat  39130  cdlemd9  39163  cdleme21h  39291  cdlemg7fvbwN  39564  cdlemg7aN  39582  cdlemg34  39669  cdlemg36  39671  cdlemg44  39690  cdlemg48  39694  tendo1ne0  39785  cdlemk26-3  39863  cdlemk55b  39917  cdleml4N  39936  dih1dimatlem0  40285  dihglblem6  40297  dochshpncl  40341  dvh4dimlem  40400  dvh3dim2  40405  dvh3dim3N  40406  dochsatshpb  40409  dochexmidlem4  40420  dochexmidlem5  40421  dochexmidlem8  40424  dochkr1  40435  dochkr1OLDN  40436  lcfl7lem  40456  lcfl6  40457  lcfl8  40459  lcfrlem16  40515  lcfrlem40  40539  mapdval2N  40587  mapdrvallem2  40602  mapdpglem24  40661  mapdh6iN  40701  mapdh8ad  40736  mapdh8e  40741  hdmap1l6i  40775  hdmapval0  40790  hdmapevec  40792  hdmapval3N  40795  hdmap10lem  40796  hdmap11lem2  40799  hdmaprnlem15N  40818  hdmaprnlem16N  40819  hdmap14lem10  40834  hdmap14lem11  40835  hdmap14lem12  40836  hdmap14lem14  40838  hgmapval0  40849  hgmapval1  40850  hgmapadd  40851  hgmapmul  40852  hgmaprnlem3N  40855  hgmaprnlem4N  40856  hgmap11  40859  hgmapvvlem3  40882  rpnnen3lem  41852  onexlimgt  42074  grumnudlem  43126  dvconstbi  43175  expgrowth  43176  eliuniin  43870  wessf1ornlem  43963  limccog  44415  0ellimcdiv  44444  cosknegpi  44664  cncfshift  44669  cncfperiod  44674  cncfuni  44681  icccncfext  44682  dvbdfbdioolem1  44723  itgperiod  44776  stoweidlem57  44852  fourierdlem12  44914  fourierdlem48  44949  fourierdlem49  44950  fourierdlem52  44953  fourierdlem54  44955  fourierdlem68  44969  fourierdlem77  44978  fourierdlem83  44984  fourierdlem87  44988  fourierdlem102  45003  fourierdlem103  45004  fourierdlem104  45005  fourierdlem113  45014  fourierdlem114  45015  elaa2  45029  etransclem24  45053  etransclem32  45061  etransclem48  45077  ovolval5lem3  45449  sigarcol  45659  f1oresf1o2  46078  imaelsetpreimafv  46142