Theorem rexlimdv3a 3249

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

Syntax hints:   → wi 4   ∧ w3a 1080   ∈ wcel 2081  ∃wrex 3106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1082  df-ex 1762  df-ral 3110  df-rex 3111

This theorem is referenced by:  sorpssuni  7316  sorpssint  7317  mapsnd  8299  tcrank  9159  rpnnen1lem5  12230  hashfun  13646  resqrex  14444  resqrtcl  14447  fprodle  15183  prmgaplem6  16221  lbsextlem3  19622  cmpsublem  21691  cmpcld  21694  ovoliunlem2  23787  isblo3i  28269  trisegint  33098  itg2addnclem  34474  areacirclem2  34514  lshpnelb  35651  lsatfixedN  35676  lsmsatcv  35677  lssatomic  35678  lcv1  35708  lsatcvatlem  35716  islshpcv  35720  lfl1  35737  lshpsmreu  35776  lshpkrex  35785  lshpset2N  35786  lkrlspeqN  35838  cvrval3  36080  1cvratlt  36141  ps-2b  36149  llnnleat  36180  lvolex3N  36205  lplncvrlvol2  36282  osumcllem7N  36629  lhp0lt  36670  lhpj1  36689  4atexlemex6  36741  4atexlem7  36742  trlnidat  36840  cdlemd9  36873  cdleme21h  37001  cdlemg7fvbwN  37274  cdlemg7aN  37292  cdlemg34  37379  cdlemg36  37381  cdlemg44  37400  cdlemg48  37404  tendo1ne0  37495  cdlemk26-3  37573  cdlemk55b  37627  cdleml4N  37646  dih1dimatlem0  37995  dihglblem6  38007  dochshpncl  38051  dvh4dimlem  38110  dvh3dim2  38115  dvh3dim3N  38116  dochsatshpb  38119  dochexmidlem4  38130  dochexmidlem5  38131  dochexmidlem8  38134  dochkr1  38145  dochkr1OLDN  38146  lcfl7lem  38166  lcfl6  38167  lcfl8  38169  lcfrlem16  38225  lcfrlem40  38249  mapdval2N  38297  mapdrvallem2  38312  mapdpglem24  38371  mapdh6iN  38411  mapdh8ad  38446  mapdh8e  38451  hdmap1l6i  38485  hdmapval0  38500  hdmapevec  38502  hdmapval3N  38505  hdmap10lem  38506  hdmap11lem2  38509  hdmaprnlem15N  38528  hdmaprnlem16N  38529  hdmap14lem10  38544  hdmap14lem11  38545  hdmap14lem12  38546  hdmap14lem14  38548  hgmapval0  38559  hgmapval1  38560  hgmapadd  38561  hgmapmul  38562  hgmaprnlem3N  38565  hgmaprnlem4N  38566  hgmap11  38569  hgmapvvlem3  38592  rpnnen3lem  39113  grumnudlem  40118  dvconstbi  40204  expgrowth  40205  eliuniin  40904  wessf1ornlem  40985  limccog  41443  0ellimcdiv  41472  cosknegpi  41691  cncfshift  41698  cncfperiod  41703  cncfuni  41710  icccncfext  41711  dvbdfbdioolem1  41754  itgperiod  41807  stoweidlem57  41884  fourierdlem12  41946  fourierdlem48  41981  fourierdlem49  41982  fourierdlem52  41985  fourierdlem54  41987  fourierdlem68  42001  fourierdlem77  42010  fourierdlem83  42016  fourierdlem87  42020  fourierdlem102  42035  fourierdlem103  42036  fourierdlem104  42037  fourierdlem113  42046  fourierdlem114  42047  elaa2  42061  etransclem24  42085  etransclem32  42093  etransclem48  42109  sigarcol  42663  f1oresf1o2  43006