Theorem rexlimdv3a 3142

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

Syntax hints:   → wi 4   ∧ w3a 1087   ∈ wcel 2114  ∃wrex 3061

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 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1782  df-rex 3062

This theorem is referenced by:  sorpssuni  7686  sorpssint  7687  mapsnd  8834  tcrank  9808  rpnnen1lem5  12931  hashfun  14399  resqrex  15212  resqrtcl  15215  fprodle  15961  prmgaplem6  17027  lbsextlem3  21158  cmpsublem  23364  cmpcld  23367  ovoliunlem2  25470  isblo3i  30872  trisegint  36210  itg2addnclem  37992  areacirclem2  38030  lshpnelb  39430  lsatfixedN  39455  lsmsatcv  39456  lssatomic  39457  lcv1  39487  lsatcvatlem  39495  islshpcv  39499  lfl1  39516  lshpsmreu  39555  lshpkrex  39564  lshpset2N  39565  lkrlspeqN  39617  cvrval3  39859  1cvratlt  39920  ps-2b  39928  llnnleat  39959  lvolex3N  39984  lplncvrlvol2  40061  osumcllem7N  40408  lhp0lt  40449  lhpj1  40468  4atexlemex6  40520  4atexlem7  40521  trlnidat  40619  cdlemd9  40652  cdleme21h  40780  cdlemg7fvbwN  41053  cdlemg7aN  41071  cdlemg34  41158  cdlemg36  41160  cdlemg44  41179  cdlemg48  41183  tendo1ne0  41274  cdlemk26-3  41352  cdlemk55b  41406  cdleml4N  41425  dih1dimatlem0  41774  dihglblem6  41786  dochshpncl  41830  dvh4dimlem  41889  dvh3dim2  41894  dvh3dim3N  41895  dochsatshpb  41898  dochexmidlem4  41909  dochexmidlem5  41910  dochexmidlem8  41913  dochkr1  41924  dochkr1OLDN  41925  lcfl7lem  41945  lcfl6  41946  lcfl8  41948  lcfrlem16  42004  lcfrlem40  42028  mapdval2N  42076  mapdrvallem2  42091  mapdpglem24  42150  mapdh6iN  42190  mapdh8ad  42225  mapdh8e  42230  hdmap1l6i  42264  hdmapval0  42279  hdmapevec  42281  hdmapval3N  42284  hdmap10lem  42285  hdmap11lem2  42288  hdmaprnlem15N  42307  hdmaprnlem16N  42308  hdmap14lem10  42323  hdmap14lem11  42324  hdmap14lem12  42325  hdmap14lem14  42327  hgmapval0  42338  hgmapval1  42339  hgmapadd  42340  hgmapmul  42341  hgmaprnlem3N  42344  hgmaprnlem4N  42345  hgmap11  42348  hgmapvvlem3  42371  rpnnen3lem  43459  onexlimgt  43671  grumnudlem  44712  dvconstbi  44761  expgrowth  44762  eliuniin  45529  wessf1ornlem  45615  ssmapsn  45645  limccog  46050  0ellimcdiv  46077  cosknegpi  46297  cncfshift  46302  cncfperiod  46307  cncfuni  46314  icccncfext  46315  dvbdfbdioolem1  46356  itgperiod  46409  stoweidlem57  46485  fourierdlem12  46547  fourierdlem48  46582  fourierdlem49  46583  fourierdlem52  46586  fourierdlem54  46588  fourierdlem68  46602  fourierdlem77  46611  fourierdlem83  46617  fourierdlem87  46621  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem113  46647  fourierdlem114  46648  elaa2  46662  etransclem24  46686  etransclem32  46694  etransclem48  46710  ovolval5lem3  47082  sigarcol  47292  f1oresf1o2  47739  imaelsetpreimafv  47855  uhgrimisgrgriclem  48406