Theorem rexlimdv3a 3198

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

Syntax hints:   → wi 4   ∧ w3a 1089   ∈ wcel 2110  ∃wrex 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1091  df-ex 1788  df-ral 3059  df-rex 3060

This theorem is referenced by:  sorpssuni  7509  sorpssint  7510  mapsnd  8556  tcrank  9483  rpnnen1lem5  12560  hashfun  13987  resqrex  14797  resqrtcl  14800  fprodle  15539  prmgaplem6  16590  lbsextlem3  20169  cmpsublem  22268  cmpcld  22271  ovoliunlem2  24372  isblo3i  28854  trisegint  34024  itg2addnclem  35522  areacirclem2  35560  lshpnelb  36692  lsatfixedN  36717  lsmsatcv  36718  lssatomic  36719  lcv1  36749  lsatcvatlem  36757  islshpcv  36761  lfl1  36778  lshpsmreu  36817  lshpkrex  36826  lshpset2N  36827  lkrlspeqN  36879  cvrval3  37121  1cvratlt  37182  ps-2b  37190  llnnleat  37221  lvolex3N  37246  lplncvrlvol2  37323  osumcllem7N  37670  lhp0lt  37711  lhpj1  37730  4atexlemex6  37782  4atexlem7  37783  trlnidat  37881  cdlemd9  37914  cdleme21h  38042  cdlemg7fvbwN  38315  cdlemg7aN  38333  cdlemg34  38420  cdlemg36  38422  cdlemg44  38441  cdlemg48  38445  tendo1ne0  38536  cdlemk26-3  38614  cdlemk55b  38668  cdleml4N  38687  dih1dimatlem0  39036  dihglblem6  39048  dochshpncl  39092  dvh4dimlem  39151  dvh3dim2  39156  dvh3dim3N  39157  dochsatshpb  39160  dochexmidlem4  39171  dochexmidlem5  39172  dochexmidlem8  39175  dochkr1  39186  dochkr1OLDN  39187  lcfl7lem  39207  lcfl6  39208  lcfl8  39210  lcfrlem16  39266  lcfrlem40  39290  mapdval2N  39338  mapdrvallem2  39353  mapdpglem24  39412  mapdh6iN  39452  mapdh8ad  39487  mapdh8e  39492  hdmap1l6i  39526  hdmapval0  39541  hdmapevec  39543  hdmapval3N  39546  hdmap10lem  39547  hdmap11lem2  39550  hdmaprnlem15N  39569  hdmaprnlem16N  39570  hdmap14lem10  39585  hdmap14lem11  39586  hdmap14lem12  39587  hdmap14lem14  39589  hgmapval0  39600  hgmapval1  39601  hgmapadd  39602  hgmapmul  39603  hgmaprnlem3N  39606  hgmaprnlem4N  39607  hgmap11  39610  hgmapvvlem3  39633  rpnnen3lem  40508  grumnudlem  41528  dvconstbi  41577  expgrowth  41578  eliuniin  42274  wessf1ornlem  42347  limccog  42790  0ellimcdiv  42819  cosknegpi  43039  cncfshift  43044  cncfperiod  43049  cncfuni  43056  icccncfext  43057  dvbdfbdioolem1  43098  itgperiod  43151  stoweidlem57  43227  fourierdlem12  43289  fourierdlem48  43324  fourierdlem49  43325  fourierdlem52  43328  fourierdlem54  43330  fourierdlem68  43344  fourierdlem77  43353  fourierdlem83  43359  fourierdlem87  43363  fourierdlem102  43378  fourierdlem103  43379  fourierdlem104  43380  fourierdlem113  43389  fourierdlem114  43390  elaa2  43404  etransclem24  43428  etransclem32  43436  etransclem48  43452  sigarcol  44006  f1oresf1o2  44409  imaelsetpreimafv  44474