Theorem rexlimdv3a 3138

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

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

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 3054

This theorem is referenced by:  sorpssuni  7708  sorpssint  7709  mapsnd  8859  tcrank  9837  rpnnen1lem5  12940  hashfun  14402  resqrex  15216  resqrtcl  15219  fprodle  15962  prmgaplem6  17027  lbsextlem3  21070  cmpsublem  23286  cmpcld  23289  ovoliunlem2  25404  isblo3i  30730  trisegint  36016  itg2addnclem  37665  areacirclem2  37703  lshpnelb  38977  lsatfixedN  39002  lsmsatcv  39003  lssatomic  39004  lcv1  39034  lsatcvatlem  39042  islshpcv  39046  lfl1  39063  lshpsmreu  39102  lshpkrex  39111  lshpset2N  39112  lkrlspeqN  39164  cvrval3  39407  1cvratlt  39468  ps-2b  39476  llnnleat  39507  lvolex3N  39532  lplncvrlvol2  39609  osumcllem7N  39956  lhp0lt  39997  lhpj1  40016  4atexlemex6  40068  4atexlem7  40069  trlnidat  40167  cdlemd9  40200  cdleme21h  40328  cdlemg7fvbwN  40601  cdlemg7aN  40619  cdlemg34  40706  cdlemg36  40708  cdlemg44  40727  cdlemg48  40731  tendo1ne0  40822  cdlemk26-3  40900  cdlemk55b  40954  cdleml4N  40973  dih1dimatlem0  41322  dihglblem6  41334  dochshpncl  41378  dvh4dimlem  41437  dvh3dim2  41442  dvh3dim3N  41443  dochsatshpb  41446  dochexmidlem4  41457  dochexmidlem5  41458  dochexmidlem8  41461  dochkr1  41472  dochkr1OLDN  41473  lcfl7lem  41493  lcfl6  41494  lcfl8  41496  lcfrlem16  41552  lcfrlem40  41576  mapdval2N  41624  mapdrvallem2  41639  mapdpglem24  41698  mapdh6iN  41738  mapdh8ad  41773  mapdh8e  41778  hdmap1l6i  41812  hdmapval0  41827  hdmapevec  41829  hdmapval3N  41832  hdmap10lem  41833  hdmap11lem2  41836  hdmaprnlem15N  41855  hdmaprnlem16N  41856  hdmap14lem10  41871  hdmap14lem11  41872  hdmap14lem12  41873  hdmap14lem14  41875  hgmapval0  41886  hgmapval1  41887  hgmapadd  41888  hgmapmul  41889  hgmaprnlem3N  41892  hgmaprnlem4N  41893  hgmap11  41896  hgmapvvlem3  41919  rpnnen3lem  43020  onexlimgt  43232  grumnudlem  44274  dvconstbi  44323  expgrowth  44324  eliuniin  45093  wessf1ornlem  45179  ssmapsn  45210  limccog  45618  0ellimcdiv  45647  cosknegpi  45867  cncfshift  45872  cncfperiod  45877  cncfuni  45884  icccncfext  45885  dvbdfbdioolem1  45926  itgperiod  45979  stoweidlem57  46055  fourierdlem12  46117  fourierdlem48  46152  fourierdlem49  46153  fourierdlem52  46156  fourierdlem54  46158  fourierdlem68  46172  fourierdlem77  46181  fourierdlem83  46187  fourierdlem87  46191  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem113  46217  fourierdlem114  46218  elaa2  46232  etransclem24  46256  etransclem32  46264  etransclem48  46280  ovolval5lem3  46652  sigarcol  46862  f1oresf1o2  47292  imaelsetpreimafv  47396  uhgrimisgrgriclem  47930