Theorem rexlimdv3a 3141

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

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2113  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  sorpssuni  7677  sorpssint  7678  mapsnd  8824  tcrank  9796  rpnnen1lem5  12894  hashfun  14360  resqrex  15173  resqrtcl  15176  fprodle  15919  prmgaplem6  16984  lbsextlem3  21115  cmpsublem  23343  cmpcld  23346  ovoliunlem2  25460  isblo3i  30876  trisegint  36222  itg2addnclem  37868  areacirclem2  37906  lshpnelb  39240  lsatfixedN  39265  lsmsatcv  39266  lssatomic  39267  lcv1  39297  lsatcvatlem  39305  islshpcv  39309  lfl1  39326  lshpsmreu  39365  lshpkrex  39374  lshpset2N  39375  lkrlspeqN  39427  cvrval3  39669  1cvratlt  39730  ps-2b  39738  llnnleat  39769  lvolex3N  39794  lplncvrlvol2  39871  osumcllem7N  40218  lhp0lt  40259  lhpj1  40278  4atexlemex6  40330  4atexlem7  40331  trlnidat  40429  cdlemd9  40462  cdleme21h  40590  cdlemg7fvbwN  40863  cdlemg7aN  40881  cdlemg34  40968  cdlemg36  40970  cdlemg44  40989  cdlemg48  40993  tendo1ne0  41084  cdlemk26-3  41162  cdlemk55b  41216  cdleml4N  41235  dih1dimatlem0  41584  dihglblem6  41596  dochshpncl  41640  dvh4dimlem  41699  dvh3dim2  41704  dvh3dim3N  41705  dochsatshpb  41708  dochexmidlem4  41719  dochexmidlem5  41720  dochexmidlem8  41723  dochkr1  41734  dochkr1OLDN  41735  lcfl7lem  41755  lcfl6  41756  lcfl8  41758  lcfrlem16  41814  lcfrlem40  41838  mapdval2N  41886  mapdrvallem2  41901  mapdpglem24  41960  mapdh6iN  42000  mapdh8ad  42035  mapdh8e  42040  hdmap1l6i  42074  hdmapval0  42089  hdmapevec  42091  hdmapval3N  42094  hdmap10lem  42095  hdmap11lem2  42098  hdmaprnlem15N  42117  hdmaprnlem16N  42118  hdmap14lem10  42133  hdmap14lem11  42134  hdmap14lem12  42135  hdmap14lem14  42137  hgmapval0  42148  hgmapval1  42149  hgmapadd  42150  hgmapmul  42151  hgmaprnlem3N  42154  hgmaprnlem4N  42155  hgmap11  42158  hgmapvvlem3  42181  rpnnen3lem  43269  onexlimgt  43481  grumnudlem  44522  dvconstbi  44571  expgrowth  44572  eliuniin  45339  wessf1ornlem  45425  ssmapsn  45456  limccog  45862  0ellimcdiv  45889  cosknegpi  46109  cncfshift  46114  cncfperiod  46119  cncfuni  46126  icccncfext  46127  dvbdfbdioolem1  46168  itgperiod  46221  stoweidlem57  46297  fourierdlem12  46359  fourierdlem48  46394  fourierdlem49  46395  fourierdlem52  46398  fourierdlem54  46400  fourierdlem68  46414  fourierdlem77  46423  fourierdlem83  46429  fourierdlem87  46433  fourierdlem102  46448  fourierdlem103  46449  fourierdlem104  46450  fourierdlem113  46459  fourierdlem114  46460  elaa2  46474  etransclem24  46498  etransclem32  46506  etransclem48  46522  ovolval5lem3  46894  sigarcol  47104  f1oresf1o2  47533  imaelsetpreimafv  47637  uhgrimisgrgriclem  48172