Theorem rexlimdv3a 3173

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   ∈ wcel 2146  ∃wrex 3092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1813  df-rex 3093

This theorem is used by:  sorpssuni  7742  sorpssint  7743  mapsnd  8893  tcrank  9866  rpnnen1lem5  13023  hashfun  14494  resqrex  15327  resqrtcl  15330  fprodle  16076  prmgaplem6  17141  lbsextlem3  21321  cmpsublem  23593  cmpcld  23596  ovoliunlem2  25699  isblo3i  31190  trisegint  36541  itg2addnclem  38363  areacirclem2  38401  lshpnelb  39799  lsatfixedN  39824  lsmsatcv  39825  lssatomic  39826  lcv1  39856  lsatcvatlem  39864  islshpcv  39868  lfl1  39885  lshpsmreu  39924  lshpkrex  39933  lshpset2N  39934  lkrlspeqN  39986  cvrval3  40228  1cvratlt  40289  ps-2b  40297  llnnleat  40328  lvolex3N  40353  lplncvrlvol2  40430  osumcllem7N  40777  lhp0lt  40818  lhpj1  40837  4atexlemex6  40889  4atexlem7  40890  trlnidat  40988  cdlemd9  41021  cdleme21h  41149  cdlemg7fvbwN  41422  cdlemg7aN  41440  cdlemg34  41527  cdlemg36  41529  cdlemg44  41548  cdlemg48  41552  tendo1ne0  41643  cdlemk26-3  41721  cdlemk55b  41775  cdleml4N  41794  dih1dimatlem0  42143  dihglblem6  42155  dochshpncl  42199  dvh4dimlem  42258  dvh3dim2  42263  dvh3dim3N  42264  dochsatshpb  42267  dochexmidlem4  42278  dochexmidlem5  42279  dochexmidlem8  42282  dochkr1  42293  dochkr1OLDN  42294  lcfl7lem  42314  lcfl6  42315  lcfl8  42317  lcfrlem16  42373  lcfrlem40  42397  mapdval2N  42445  mapdrvallem2  42460  mapdpglem24  42519  mapdh6iN  42559  mapdh8ad  42594  mapdh8e  42599  hdmap1l6i  42633  hdmapval0  42648  hdmapevec  42650  hdmapval3N  42653  hdmap10lem  42654  hdmap11lem2  42657  hdmaprnlem15N  42676  hdmaprnlem16N  42677  hdmap14lem10  42692  hdmap14lem11  42693  hdmap14lem12  42694  hdmap14lem14  42696  hgmapval0  42707  hgmapval1  42708  hgmapadd  42709  hgmapmul  42710  hgmaprnlem3N  42713  hgmaprnlem4N  42714  hgmap11  42717  hgmapvvlem3  42740  rpnnen3lem  43799  onexlimgt  44011  grumnudlem  45036  dvconstbi  45085  expgrowth  45086  eliuniin  45858  wessf1ornlem  45944  ssmapsn  45973  limccog  46377  0ellimcdiv  46404  cosknegpi  46624  cncfshift  46629  cncfperiod  46634  cncfuni  46641  icccncfext  46642  dvbdfbdioolem1  46683  itgperiod  46736  stoweidlem57  46812  fourierdlem12  46874  fourierdlem48  46909  fourierdlem49  46910  fourierdlem52  46913  fourierdlem54  46915  fourierdlem68  46929  fourierdlem77  46938  fourierdlem83  46944  fourierdlem87  46948  fourierdlem102  46963  fourierdlem103  46964  fourierdlem104  46965  fourierdlem113  46974  fourierdlem114  46975  elaa2  46989  etransclem24  47013  etransclem32  47021  etransclem48  47037  ovolval5lem3  47409  sssmf  47493  sigarcol  47619  f1oresf1o2  48069  imaelsetpreimafv  48185  uhgrimisgrgriclem  48736