Theorem rexlimdv3a 3157

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

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2106  ∃wrex 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908

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

This theorem is referenced by:  sorpssuni  7751  sorpssint  7752  mapsnd  8925  tcrank  9922  rpnnen1lem5  13021  hashfun  14473  resqrex  15286  resqrtcl  15289  fprodle  16029  prmgaplem6  17090  lbsextlem3  21180  cmpsublem  23423  cmpcld  23426  ovoliunlem2  25552  isblo3i  30830  trisegint  36010  itg2addnclem  37658  areacirclem2  37696  lshpnelb  38966  lsatfixedN  38991  lsmsatcv  38992  lssatomic  38993  lcv1  39023  lsatcvatlem  39031  islshpcv  39035  lfl1  39052  lshpsmreu  39091  lshpkrex  39100  lshpset2N  39101  lkrlspeqN  39153  cvrval3  39396  1cvratlt  39457  ps-2b  39465  llnnleat  39496  lvolex3N  39521  lplncvrlvol2  39598  osumcllem7N  39945  lhp0lt  39986  lhpj1  40005  4atexlemex6  40057  4atexlem7  40058  trlnidat  40156  cdlemd9  40189  cdleme21h  40317  cdlemg7fvbwN  40590  cdlemg7aN  40608  cdlemg34  40695  cdlemg36  40697  cdlemg44  40716  cdlemg48  40720  tendo1ne0  40811  cdlemk26-3  40889  cdlemk55b  40943  cdleml4N  40962  dih1dimatlem0  41311  dihglblem6  41323  dochshpncl  41367  dvh4dimlem  41426  dvh3dim2  41431  dvh3dim3N  41432  dochsatshpb  41435  dochexmidlem4  41446  dochexmidlem5  41447  dochexmidlem8  41450  dochkr1  41461  dochkr1OLDN  41462  lcfl7lem  41482  lcfl6  41483  lcfl8  41485  lcfrlem16  41541  lcfrlem40  41565  mapdval2N  41613  mapdrvallem2  41628  mapdpglem24  41687  mapdh6iN  41727  mapdh8ad  41762  mapdh8e  41767  hdmap1l6i  41801  hdmapval0  41816  hdmapevec  41818  hdmapval3N  41821  hdmap10lem  41822  hdmap11lem2  41825  hdmaprnlem15N  41844  hdmaprnlem16N  41845  hdmap14lem10  41860  hdmap14lem11  41861  hdmap14lem12  41862  hdmap14lem14  41864  hgmapval0  41875  hgmapval1  41876  hgmapadd  41877  hgmapmul  41878  hgmaprnlem3N  41881  hgmaprnlem4N  41882  hgmap11  41885  hgmapvvlem3  41908  rpnnen3lem  43020  onexlimgt  43232  grumnudlem  44281  dvconstbi  44330  expgrowth  44331  eliuniin  45039  wessf1ornlem  45128  ssmapsn  45159  limccog  45576  0ellimcdiv  45605  cosknegpi  45825  cncfshift  45830  cncfperiod  45835  cncfuni  45842  icccncfext  45843  dvbdfbdioolem1  45884  itgperiod  45937  stoweidlem57  46013  fourierdlem12  46075  fourierdlem48  46110  fourierdlem49  46111  fourierdlem52  46114  fourierdlem54  46116  fourierdlem68  46130  fourierdlem77  46139  fourierdlem83  46145  fourierdlem87  46149  fourierdlem102  46164  fourierdlem103  46165  fourierdlem104  46166  fourierdlem113  46175  fourierdlem114  46176  elaa2  46190  etransclem24  46214  etransclem32  46222  etransclem48  46238  ovolval5lem3  46610  sigarcol  46820  f1oresf1o2  47241  imaelsetpreimafv  47320  uhgrimisgrgriclem  47836