Theorem rexlimdv3a 3165

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

Syntax hints:   → wi 4   ∧ w3a 1087   ∈ wcel 2108  ∃wrex 3076

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1778  df-rex 3077

This theorem is referenced by:  sorpssuni  7767  sorpssint  7768  mapsnd  8944  tcrank  9953  rpnnen1lem5  13046  hashfun  14486  resqrex  15299  resqrtcl  15302  fprodle  16044  prmgaplem6  17103  lbsextlem3  21185  cmpsublem  23428  cmpcld  23431  ovoliunlem2  25557  isblo3i  30833  trisegint  35992  itg2addnclem  37631  areacirclem2  37669  lshpnelb  38940  lsatfixedN  38965  lsmsatcv  38966  lssatomic  38967  lcv1  38997  lsatcvatlem  39005  islshpcv  39009  lfl1  39026  lshpsmreu  39065  lshpkrex  39074  lshpset2N  39075  lkrlspeqN  39127  cvrval3  39370  1cvratlt  39431  ps-2b  39439  llnnleat  39470  lvolex3N  39495  lplncvrlvol2  39572  osumcllem7N  39919  lhp0lt  39960  lhpj1  39979  4atexlemex6  40031  4atexlem7  40032  trlnidat  40130  cdlemd9  40163  cdleme21h  40291  cdlemg7fvbwN  40564  cdlemg7aN  40582  cdlemg34  40669  cdlemg36  40671  cdlemg44  40690  cdlemg48  40694  tendo1ne0  40785  cdlemk26-3  40863  cdlemk55b  40917  cdleml4N  40936  dih1dimatlem0  41285  dihglblem6  41297  dochshpncl  41341  dvh4dimlem  41400  dvh3dim2  41405  dvh3dim3N  41406  dochsatshpb  41409  dochexmidlem4  41420  dochexmidlem5  41421  dochexmidlem8  41424  dochkr1  41435  dochkr1OLDN  41436  lcfl7lem  41456  lcfl6  41457  lcfl8  41459  lcfrlem16  41515  lcfrlem40  41539  mapdval2N  41587  mapdrvallem2  41602  mapdpglem24  41661  mapdh6iN  41701  mapdh8ad  41736  mapdh8e  41741  hdmap1l6i  41775  hdmapval0  41790  hdmapevec  41792  hdmapval3N  41795  hdmap10lem  41796  hdmap11lem2  41799  hdmaprnlem15N  41818  hdmaprnlem16N  41819  hdmap14lem10  41834  hdmap14lem11  41835  hdmap14lem12  41836  hdmap14lem14  41838  hgmapval0  41849  hgmapval1  41850  hgmapadd  41851  hgmapmul  41852  hgmaprnlem3N  41855  hgmaprnlem4N  41856  hgmap11  41859  hgmapvvlem3  41882  rpnnen3lem  42988  onexlimgt  43204  grumnudlem  44254  dvconstbi  44303  expgrowth  44304  eliuniin  45001  wessf1ornlem  45092  limccog  45541  0ellimcdiv  45570  cosknegpi  45790  cncfshift  45795  cncfperiod  45800  cncfuni  45807  icccncfext  45808  dvbdfbdioolem1  45849  itgperiod  45902  stoweidlem57  45978  fourierdlem12  46040  fourierdlem48  46075  fourierdlem49  46076  fourierdlem52  46079  fourierdlem54  46081  fourierdlem68  46095  fourierdlem77  46104  fourierdlem83  46110  fourierdlem87  46114  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem113  46140  fourierdlem114  46141  elaa2  46155  etransclem24  46179  etransclem32  46187  etransclem48  46203  ovolval5lem3  46575  sigarcol  46785  f1oresf1o2  47206  imaelsetpreimafv  47269  uhgrimisgrgriclem  47782