Theorem rexlimdv3a 3158

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

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2105  ∃wrex 3069

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1088  df-ex 1781  df-rex 3070

This theorem is referenced by:  sorpssuni  7725  sorpssint  7726  mapsnd  8883  tcrank  9882  rpnnen1lem5  12970  hashfun  14402  resqrex  15202  resqrtcl  15205  fprodle  15945  prmgaplem6  16994  lbsextlem3  20919  cmpsublem  23124  cmpcld  23127  ovoliunlem2  25253  isblo3i  30318  trisegint  35301  itg2addnclem  36843  areacirclem2  36881  lshpnelb  38158  lsatfixedN  38183  lsmsatcv  38184  lssatomic  38185  lcv1  38215  lsatcvatlem  38223  islshpcv  38227  lfl1  38244  lshpsmreu  38283  lshpkrex  38292  lshpset2N  38293  lkrlspeqN  38345  cvrval3  38588  1cvratlt  38649  ps-2b  38657  llnnleat  38688  lvolex3N  38713  lplncvrlvol2  38790  osumcllem7N  39137  lhp0lt  39178  lhpj1  39197  4atexlemex6  39249  4atexlem7  39250  trlnidat  39348  cdlemd9  39381  cdleme21h  39509  cdlemg7fvbwN  39782  cdlemg7aN  39800  cdlemg34  39887  cdlemg36  39889  cdlemg44  39908  cdlemg48  39912  tendo1ne0  40003  cdlemk26-3  40081  cdlemk55b  40135  cdleml4N  40154  dih1dimatlem0  40503  dihglblem6  40515  dochshpncl  40559  dvh4dimlem  40618  dvh3dim2  40623  dvh3dim3N  40624  dochsatshpb  40627  dochexmidlem4  40638  dochexmidlem5  40639  dochexmidlem8  40642  dochkr1  40653  dochkr1OLDN  40654  lcfl7lem  40674  lcfl6  40675  lcfl8  40677  lcfrlem16  40733  lcfrlem40  40757  mapdval2N  40805  mapdrvallem2  40820  mapdpglem24  40879  mapdh6iN  40919  mapdh8ad  40954  mapdh8e  40959  hdmap1l6i  40993  hdmapval0  41008  hdmapevec  41010  hdmapval3N  41013  hdmap10lem  41014  hdmap11lem2  41017  hdmaprnlem15N  41036  hdmaprnlem16N  41037  hdmap14lem10  41052  hdmap14lem11  41053  hdmap14lem12  41054  hdmap14lem14  41056  hgmapval0  41067  hgmapval1  41068  hgmapadd  41069  hgmapmul  41070  hgmaprnlem3N  41073  hgmaprnlem4N  41074  hgmap11  41077  hgmapvvlem3  41100  rpnnen3lem  42073  onexlimgt  42295  grumnudlem  43347  dvconstbi  43396  expgrowth  43397  eliuniin  44091  wessf1ornlem  44184  limccog  44636  0ellimcdiv  44665  cosknegpi  44885  cncfshift  44890  cncfperiod  44895  cncfuni  44902  icccncfext  44903  dvbdfbdioolem1  44944  itgperiod  44997  stoweidlem57  45073  fourierdlem12  45135  fourierdlem48  45170  fourierdlem49  45171  fourierdlem52  45174  fourierdlem54  45176  fourierdlem68  45190  fourierdlem77  45199  fourierdlem83  45205  fourierdlem87  45209  fourierdlem102  45224  fourierdlem103  45225  fourierdlem104  45226  fourierdlem113  45235  fourierdlem114  45236  elaa2  45250  etransclem24  45274  etransclem32  45282  etransclem48  45298  ovolval5lem3  45670  sigarcol  45880  f1oresf1o2  46299  imaelsetpreimafv  46363