Theorem rexlimdv3a 3158

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

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2107  ∃wrex 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

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

This theorem is referenced by:  sorpssuni  7753  sorpssint  7754  mapsnd  8927  tcrank  9925  rpnnen1lem5  13024  hashfun  14477  resqrex  15290  resqrtcl  15293  fprodle  16033  prmgaplem6  17095  lbsextlem3  21163  cmpsublem  23408  cmpcld  23411  ovoliunlem2  25539  isblo3i  30821  trisegint  36030  itg2addnclem  37679  areacirclem2  37717  lshpnelb  38986  lsatfixedN  39011  lsmsatcv  39012  lssatomic  39013  lcv1  39043  lsatcvatlem  39051  islshpcv  39055  lfl1  39072  lshpsmreu  39111  lshpkrex  39120  lshpset2N  39121  lkrlspeqN  39173  cvrval3  39416  1cvratlt  39477  ps-2b  39485  llnnleat  39516  lvolex3N  39541  lplncvrlvol2  39618  osumcllem7N  39965  lhp0lt  40006  lhpj1  40025  4atexlemex6  40077  4atexlem7  40078  trlnidat  40176  cdlemd9  40209  cdleme21h  40337  cdlemg7fvbwN  40610  cdlemg7aN  40628  cdlemg34  40715  cdlemg36  40717  cdlemg44  40736  cdlemg48  40740  tendo1ne0  40831  cdlemk26-3  40909  cdlemk55b  40963  cdleml4N  40982  dih1dimatlem0  41331  dihglblem6  41343  dochshpncl  41387  dvh4dimlem  41446  dvh3dim2  41451  dvh3dim3N  41452  dochsatshpb  41455  dochexmidlem4  41466  dochexmidlem5  41467  dochexmidlem8  41470  dochkr1  41481  dochkr1OLDN  41482  lcfl7lem  41502  lcfl6  41503  lcfl8  41505  lcfrlem16  41561  lcfrlem40  41585  mapdval2N  41633  mapdrvallem2  41648  mapdpglem24  41707  mapdh6iN  41747  mapdh8ad  41782  mapdh8e  41787  hdmap1l6i  41821  hdmapval0  41836  hdmapevec  41838  hdmapval3N  41841  hdmap10lem  41842  hdmap11lem2  41845  hdmaprnlem15N  41864  hdmaprnlem16N  41865  hdmap14lem10  41880  hdmap14lem11  41881  hdmap14lem12  41882  hdmap14lem14  41884  hgmapval0  41895  hgmapval1  41896  hgmapadd  41897  hgmapmul  41898  hgmaprnlem3N  41901  hgmaprnlem4N  41902  hgmap11  41905  hgmapvvlem3  41928  rpnnen3lem  43048  onexlimgt  43260  grumnudlem  44309  dvconstbi  44358  expgrowth  44359  eliuniin  45109  wessf1ornlem  45195  ssmapsn  45226  limccog  45640  0ellimcdiv  45669  cosknegpi  45889  cncfshift  45894  cncfperiod  45899  cncfuni  45906  icccncfext  45907  dvbdfbdioolem1  45948  itgperiod  46001  stoweidlem57  46077  fourierdlem12  46139  fourierdlem48  46174  fourierdlem49  46175  fourierdlem52  46178  fourierdlem54  46180  fourierdlem68  46194  fourierdlem77  46203  fourierdlem83  46209  fourierdlem87  46213  fourierdlem102  46228  fourierdlem103  46229  fourierdlem104  46230  fourierdlem113  46239  fourierdlem114  46240  elaa2  46254  etransclem24  46278  etransclem32  46286  etransclem48  46302  ovolval5lem3  46674  sigarcol  46884  f1oresf1o2  47308  imaelsetpreimafv  47387  uhgrimisgrgriclem  47903