Theorem rexlimdv3a 3146

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

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2109  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  sorpssuni  7731  sorpssint  7732  mapsnd  8905  tcrank  9903  rpnnen1lem5  13002  hashfun  14460  resqrex  15274  resqrtcl  15277  fprodle  16017  prmgaplem6  17081  lbsextlem3  21126  cmpsublem  23342  cmpcld  23345  ovoliunlem2  25461  isblo3i  30787  trisegint  36051  itg2addnclem  37700  areacirclem2  37738  lshpnelb  39007  lsatfixedN  39032  lsmsatcv  39033  lssatomic  39034  lcv1  39064  lsatcvatlem  39072  islshpcv  39076  lfl1  39093  lshpsmreu  39132  lshpkrex  39141  lshpset2N  39142  lkrlspeqN  39194  cvrval3  39437  1cvratlt  39498  ps-2b  39506  llnnleat  39537  lvolex3N  39562  lplncvrlvol2  39639  osumcllem7N  39986  lhp0lt  40027  lhpj1  40046  4atexlemex6  40098  4atexlem7  40099  trlnidat  40197  cdlemd9  40230  cdleme21h  40358  cdlemg7fvbwN  40631  cdlemg7aN  40649  cdlemg34  40736  cdlemg36  40738  cdlemg44  40757  cdlemg48  40761  tendo1ne0  40852  cdlemk26-3  40930  cdlemk55b  40984  cdleml4N  41003  dih1dimatlem0  41352  dihglblem6  41364  dochshpncl  41408  dvh4dimlem  41467  dvh3dim2  41472  dvh3dim3N  41473  dochsatshpb  41476  dochexmidlem4  41487  dochexmidlem5  41488  dochexmidlem8  41491  dochkr1  41502  dochkr1OLDN  41503  lcfl7lem  41523  lcfl6  41524  lcfl8  41526  lcfrlem16  41582  lcfrlem40  41606  mapdval2N  41654  mapdrvallem2  41669  mapdpglem24  41728  mapdh6iN  41768  mapdh8ad  41803  mapdh8e  41808  hdmap1l6i  41842  hdmapval0  41857  hdmapevec  41859  hdmapval3N  41862  hdmap10lem  41863  hdmap11lem2  41866  hdmaprnlem15N  41885  hdmaprnlem16N  41886  hdmap14lem10  41901  hdmap14lem11  41902  hdmap14lem12  41903  hdmap14lem14  41905  hgmapval0  41916  hgmapval1  41917  hgmapadd  41918  hgmapmul  41919  hgmaprnlem3N  41922  hgmaprnlem4N  41923  hgmap11  41926  hgmapvvlem3  41949  rpnnen3lem  43030  onexlimgt  43242  grumnudlem  44284  dvconstbi  44333  expgrowth  44334  eliuniin  45103  wessf1ornlem  45189  ssmapsn  45220  limccog  45629  0ellimcdiv  45658  cosknegpi  45878  cncfshift  45883  cncfperiod  45888  cncfuni  45895  icccncfext  45896  dvbdfbdioolem1  45937  itgperiod  45990  stoweidlem57  46066  fourierdlem12  46128  fourierdlem48  46163  fourierdlem49  46164  fourierdlem52  46167  fourierdlem54  46169  fourierdlem68  46183  fourierdlem77  46192  fourierdlem83  46198  fourierdlem87  46202  fourierdlem102  46217  fourierdlem103  46218  fourierdlem104  46219  fourierdlem113  46228  fourierdlem114  46229  elaa2  46243  etransclem24  46267  etransclem32  46275  etransclem48  46291  ovolval5lem3  46663  sigarcol  46873  f1oresf1o2  47300  imaelsetpreimafv  47389  uhgrimisgrgriclem  47923