Theorem rexlimdv3a 3134

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

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-rex 3054

This theorem is referenced by:  sorpssuni  7672  sorpssint  7673  mapsnd  8820  tcrank  9799  rpnnen1lem5  12900  hashfun  14362  resqrex  15175  resqrtcl  15178  fprodle  15921  prmgaplem6  16986  lbsextlem3  21085  cmpsublem  23302  cmpcld  23305  ovoliunlem2  25420  isblo3i  30763  trisegint  36001  itg2addnclem  37650  areacirclem2  37688  lshpnelb  38962  lsatfixedN  38987  lsmsatcv  38988  lssatomic  38989  lcv1  39019  lsatcvatlem  39027  islshpcv  39031  lfl1  39048  lshpsmreu  39087  lshpkrex  39096  lshpset2N  39097  lkrlspeqN  39149  cvrval3  39392  1cvratlt  39453  ps-2b  39461  llnnleat  39492  lvolex3N  39517  lplncvrlvol2  39594  osumcllem7N  39941  lhp0lt  39982  lhpj1  40001  4atexlemex6  40053  4atexlem7  40054  trlnidat  40152  cdlemd9  40185  cdleme21h  40313  cdlemg7fvbwN  40586  cdlemg7aN  40604  cdlemg34  40691  cdlemg36  40693  cdlemg44  40712  cdlemg48  40716  tendo1ne0  40807  cdlemk26-3  40885  cdlemk55b  40939  cdleml4N  40958  dih1dimatlem0  41307  dihglblem6  41319  dochshpncl  41363  dvh4dimlem  41422  dvh3dim2  41427  dvh3dim3N  41428  dochsatshpb  41431  dochexmidlem4  41442  dochexmidlem5  41443  dochexmidlem8  41446  dochkr1  41457  dochkr1OLDN  41458  lcfl7lem  41478  lcfl6  41479  lcfl8  41481  lcfrlem16  41537  lcfrlem40  41561  mapdval2N  41609  mapdrvallem2  41624  mapdpglem24  41683  mapdh6iN  41723  mapdh8ad  41758  mapdh8e  41763  hdmap1l6i  41797  hdmapval0  41812  hdmapevec  41814  hdmapval3N  41817  hdmap10lem  41818  hdmap11lem2  41821  hdmaprnlem15N  41840  hdmaprnlem16N  41841  hdmap14lem10  41856  hdmap14lem11  41857  hdmap14lem12  41858  hdmap14lem14  41860  hgmapval0  41871  hgmapval1  41872  hgmapadd  41873  hgmapmul  41874  hgmaprnlem3N  41877  hgmaprnlem4N  41878  hgmap11  41881  hgmapvvlem3  41904  rpnnen3lem  43004  onexlimgt  43216  grumnudlem  44258  dvconstbi  44307  expgrowth  44308  eliuniin  45077  wessf1ornlem  45163  ssmapsn  45194  limccog  45602  0ellimcdiv  45631  cosknegpi  45851  cncfshift  45856  cncfperiod  45861  cncfuni  45868  icccncfext  45869  dvbdfbdioolem1  45910  itgperiod  45963  stoweidlem57  46039  fourierdlem12  46101  fourierdlem48  46136  fourierdlem49  46137  fourierdlem52  46140  fourierdlem54  46142  fourierdlem68  46156  fourierdlem77  46165  fourierdlem83  46171  fourierdlem87  46175  fourierdlem102  46190  fourierdlem103  46191  fourierdlem104  46192  fourierdlem113  46201  fourierdlem114  46202  elaa2  46216  etransclem24  46240  etransclem32  46248  etransclem48  46264  ovolval5lem3  46636  sigarcol  46846  f1oresf1o2  47276  imaelsetpreimafv  47380  uhgrimisgrgriclem  47915