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  7679  sorpssint  7680  mapsnd  8827  tcrank  9799  rpnnen1lem5  12922  hashfun  14390  resqrex  15203  resqrtcl  15206  fprodle  15952  prmgaplem6  17018  lbsextlem3  21150  cmpsublem  23374  cmpcld  23377  ovoliunlem2  25480  isblo3i  30887  trisegint  36226  itg2addnclem  38006  areacirclem2  38044  lshpnelb  39444  lsatfixedN  39469  lsmsatcv  39470  lssatomic  39471  lcv1  39501  lsatcvatlem  39509  islshpcv  39513  lfl1  39530  lshpsmreu  39569  lshpkrex  39578  lshpset2N  39579  lkrlspeqN  39631  cvrval3  39873  1cvratlt  39934  ps-2b  39942  llnnleat  39973  lvolex3N  39998  lplncvrlvol2  40075  osumcllem7N  40422  lhp0lt  40463  lhpj1  40482  4atexlemex6  40534  4atexlem7  40535  trlnidat  40633  cdlemd9  40666  cdleme21h  40794  cdlemg7fvbwN  41067  cdlemg7aN  41085  cdlemg34  41172  cdlemg36  41174  cdlemg44  41193  cdlemg48  41197  tendo1ne0  41288  cdlemk26-3  41366  cdlemk55b  41420  cdleml4N  41439  dih1dimatlem0  41788  dihglblem6  41800  dochshpncl  41844  dvh4dimlem  41903  dvh3dim2  41908  dvh3dim3N  41909  dochsatshpb  41912  dochexmidlem4  41923  dochexmidlem5  41924  dochexmidlem8  41927  dochkr1  41938  dochkr1OLDN  41939  lcfl7lem  41959  lcfl6  41960  lcfl8  41962  lcfrlem16  42018  lcfrlem40  42042  mapdval2N  42090  mapdrvallem2  42105  mapdpglem24  42164  mapdh6iN  42204  mapdh8ad  42239  mapdh8e  42244  hdmap1l6i  42278  hdmapval0  42293  hdmapevec  42295  hdmapval3N  42298  hdmap10lem  42299  hdmap11lem2  42302  hdmaprnlem15N  42321  hdmaprnlem16N  42322  hdmap14lem10  42337  hdmap14lem11  42338  hdmap14lem12  42339  hdmap14lem14  42341  hgmapval0  42352  hgmapval1  42353  hgmapadd  42354  hgmapmul  42355  hgmaprnlem3N  42358  hgmaprnlem4N  42359  hgmap11  42362  hgmapvvlem3  42385  rpnnen3lem  43477  onexlimgt  43689  grumnudlem  44730  dvconstbi  44779  expgrowth  44780  eliuniin  45547  wessf1ornlem  45633  ssmapsn  45663  limccog  46068  0ellimcdiv  46095  cosknegpi  46315  cncfshift  46320  cncfperiod  46325  cncfuni  46332  icccncfext  46333  dvbdfbdioolem1  46374  itgperiod  46427  stoweidlem57  46503  fourierdlem12  46565  fourierdlem48  46600  fourierdlem49  46601  fourierdlem52  46604  fourierdlem54  46606  fourierdlem68  46620  fourierdlem77  46629  fourierdlem83  46635  fourierdlem87  46639  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem113  46665  fourierdlem114  46666  elaa2  46680  etransclem24  46704  etransclem32  46712  etransclem48  46728  ovolval5lem3  47100  sigarcol  47310  f1oresf1o2  47751  imaelsetpreimafv  47867  uhgrimisgrgriclem  48418