Theorem rexlimdv3a 3143

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

Syntax hints:   → wi 4   ∧ w3a 1087   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  sorpssuni  7687  sorpssint  7688  mapsnd  8836  tcrank  9808  rpnnen1lem5  12906  hashfun  14372  resqrex  15185  resqrtcl  15188  fprodle  15931  prmgaplem6  16996  lbsextlem3  21127  cmpsublem  23355  cmpcld  23358  ovoliunlem2  25472  isblo3i  30888  trisegint  36241  itg2addnclem  37916  areacirclem2  37954  lshpnelb  39354  lsatfixedN  39379  lsmsatcv  39380  lssatomic  39381  lcv1  39411  lsatcvatlem  39419  islshpcv  39423  lfl1  39440  lshpsmreu  39479  lshpkrex  39488  lshpset2N  39489  lkrlspeqN  39541  cvrval3  39783  1cvratlt  39844  ps-2b  39852  llnnleat  39883  lvolex3N  39908  lplncvrlvol2  39985  osumcllem7N  40332  lhp0lt  40373  lhpj1  40392  4atexlemex6  40444  4atexlem7  40445  trlnidat  40543  cdlemd9  40576  cdleme21h  40704  cdlemg7fvbwN  40977  cdlemg7aN  40995  cdlemg34  41082  cdlemg36  41084  cdlemg44  41103  cdlemg48  41107  tendo1ne0  41198  cdlemk26-3  41276  cdlemk55b  41330  cdleml4N  41349  dih1dimatlem0  41698  dihglblem6  41710  dochshpncl  41754  dvh4dimlem  41813  dvh3dim2  41818  dvh3dim3N  41819  dochsatshpb  41822  dochexmidlem4  41833  dochexmidlem5  41834  dochexmidlem8  41837  dochkr1  41848  dochkr1OLDN  41849  lcfl7lem  41869  lcfl6  41870  lcfl8  41872  lcfrlem16  41928  lcfrlem40  41952  mapdval2N  42000  mapdrvallem2  42015  mapdpglem24  42074  mapdh6iN  42114  mapdh8ad  42149  mapdh8e  42154  hdmap1l6i  42188  hdmapval0  42203  hdmapevec  42205  hdmapval3N  42208  hdmap10lem  42209  hdmap11lem2  42212  hdmaprnlem15N  42231  hdmaprnlem16N  42232  hdmap14lem10  42247  hdmap14lem11  42248  hdmap14lem12  42249  hdmap14lem14  42251  hgmapval0  42262  hgmapval1  42263  hgmapadd  42264  hgmapmul  42265  hgmaprnlem3N  42268  hgmaprnlem4N  42269  hgmap11  42272  hgmapvvlem3  42295  rpnnen3lem  43382  onexlimgt  43594  grumnudlem  44635  dvconstbi  44684  expgrowth  44685  eliuniin  45452  wessf1ornlem  45538  ssmapsn  45568  limccog  45974  0ellimcdiv  46001  cosknegpi  46221  cncfshift  46226  cncfperiod  46231  cncfuni  46238  icccncfext  46239  dvbdfbdioolem1  46280  itgperiod  46333  stoweidlem57  46409  fourierdlem12  46471  fourierdlem48  46506  fourierdlem49  46507  fourierdlem52  46510  fourierdlem54  46512  fourierdlem68  46526  fourierdlem77  46535  fourierdlem83  46541  fourierdlem87  46545  fourierdlem102  46560  fourierdlem103  46561  fourierdlem104  46562  fourierdlem113  46571  fourierdlem114  46572  elaa2  46586  etransclem24  46610  etransclem32  46618  etransclem48  46634  ovolval5lem3  47006  sigarcol  47216  f1oresf1o2  47645  imaelsetpreimafv  47749  uhgrimisgrgriclem  48284