Theorem rexlimdv3a 3015

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

Syntax hints:   → wi 4   ∧ w3a 1031   ∈ wcel 1977  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033  df-ex 1696  df-ral 2901  df-rex 2902

This theorem is referenced by:  sorpssuni  6844  sorpssint  6845  tcrank  8630  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  hashfun  13084  resqrex  13839  resqrtcl  13842  prmgaplem6  15598  lbsextlem3  18981  cmpsublem  21012  cmpcld  21015  ovoliunlem2  23078  isblo3i  27040  trisegint  31305  itg2addnclem  32631  areacirclem2  32671  lshpnelb  33289  lsatfixedN  33314  lsmsatcv  33315  lssatomic  33316  lcv1  33346  lsatcvatlem  33354  islshpcv  33358  lfl1  33375  lshpsmreu  33414  lshpkrex  33423  lshpset2N  33424  lkrlspeqN  33476  cvrval3  33717  1cvratlt  33778  ps-2b  33786  llnnleat  33817  lvolex3N  33842  lplncvrlvol2  33919  osumcllem7N  34266  lhp0lt  34307  lhpj1  34326  4atexlemex6  34378  4atexlem7  34379  trlnidat  34478  cdlemd9  34511  cdleme21h  34640  cdlemg7fvbwN  34913  cdlemg7aN  34931  cdlemg34  35018  cdlemg36  35020  cdlemg44  35039  cdlemg48  35043  tendo1ne0  35134  cdlemk26-3  35212  cdlemk55b  35266  cdleml4N  35285  dih1dimatlem0  35635  dihglblem6  35647  dochshpncl  35691  dvh4dimlem  35750  dvh3dim2  35755  dvh3dim3N  35756  dochsatshpb  35759  dochexmidlem4  35770  dochexmidlem5  35771  dochexmidlem8  35774  dochkr1  35785  dochkr1OLDN  35786  lcfl7lem  35806  lcfl6  35807  lcfl8  35809  lcfrlem16  35865  lcfrlem40  35889  mapdval2N  35937  mapdrvallem2  35952  mapdpglem24  36011  mapdh6iN  36051  mapdh8ad  36086  mapdh8e  36091  hdmap1l6i  36126  hdmapval0  36143  hdmapevec  36145  hdmapval3N  36148  hdmap10lem  36149  hdmap11lem2  36152  hdmaprnlem15N  36171  hdmaprnlem16N  36172  hdmap14lem10  36187  hdmap14lem11  36188  hdmap14lem12  36189  hdmap14lem14  36191  hgmapval0  36202  hgmapval1  36203  hgmapadd  36204  hgmapmul  36205  hgmaprnlem3N  36208  hgmaprnlem4N  36209  hgmap11  36212  hgmapvvlem3  36235  rpnnen3lem  36616  dvconstbi  37555  expgrowth  37556  limccog  38687  0ellimcdiv  38716  cosknegpi  38752  cncfshift  38759  cncfperiod  38764  cncfuni  38772  icccncfext  38773  dvbdfbdioolem1  38818  itgperiod  38873  stoweidlem57  38950  fourierdlem12  39012  fourierdlem48  39047  fourierdlem49  39048  fourierdlem52  39051  fourierdlem54  39053  fourierdlem68  39067  fourierdlem77  39076  fourierdlem83  39082  fourierdlem87  39086  fourierdlem102  39101  fourierdlem103  39102  fourierdlem104  39103  fourierdlem113  39112  fourierdlem114  39113  elaa2  39127  etransclem24  39151  etransclem32  39159  etransclem48  39175  sigarcol  39702