Theorem rexlimdv3a 3170

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

Syntax hints:   → wi 4   ∧ w3a 1103   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-ex 1810  df-rex 3090

This theorem is referenced by:  sorpssuni  7731  sorpssint  7732  mapsnd  8885  tcrank  9857  rpnnen1lem5  13006  hashfun  14476  resqrex  15303  resqrtcl  15306  fprodle  16052  prmgaplem6  17117  lbsextlem3  21265  cmpsublem  23537  cmpcld  23540  ovoliunlem2  25643  isblo3i  31131  trisegint  36498  itg2addnclem  38300  areacirclem2  38338  lshpnelb  39736  lsatfixedN  39761  lsmsatcv  39762  lssatomic  39763  lcv1  39793  lsatcvatlem  39801  islshpcv  39805  lfl1  39822  lshpsmreu  39861  lshpkrex  39870  lshpset2N  39871  lkrlspeqN  39923  cvrval3  40165  1cvratlt  40226  ps-2b  40234  llnnleat  40265  lvolex3N  40290  lplncvrlvol2  40367  osumcllem7N  40714  lhp0lt  40755  lhpj1  40774  4atexlemex6  40826  4atexlem7  40827  trlnidat  40925  cdlemd9  40958  cdleme21h  41086  cdlemg7fvbwN  41359  cdlemg7aN  41377  cdlemg34  41464  cdlemg36  41466  cdlemg44  41485  cdlemg48  41489  tendo1ne0  41580  cdlemk26-3  41658  cdlemk55b  41712  cdleml4N  41731  dih1dimatlem0  42080  dihglblem6  42092  dochshpncl  42136  dvh4dimlem  42195  dvh3dim2  42200  dvh3dim3N  42201  dochsatshpb  42204  dochexmidlem4  42215  dochexmidlem5  42216  dochexmidlem8  42219  dochkr1  42230  dochkr1OLDN  42231  lcfl7lem  42251  lcfl6  42252  lcfl8  42254  lcfrlem16  42310  lcfrlem40  42334  mapdval2N  42382  mapdrvallem2  42397  mapdpglem24  42456  mapdh6iN  42496  mapdh8ad  42531  mapdh8e  42536  hdmap1l6i  42570  hdmapval0  42585  hdmapevec  42587  hdmapval3N  42590  hdmap10lem  42591  hdmap11lem2  42594  hdmaprnlem15N  42613  hdmaprnlem16N  42614  hdmap14lem10  42629  hdmap14lem11  42630  hdmap14lem12  42631  hdmap14lem14  42633  hgmapval0  42644  hgmapval1  42645  hgmapadd  42646  hgmapmul  42647  hgmaprnlem3N  42650  hgmaprnlem4N  42651  hgmap11  42654  hgmapvvlem3  42677  rpnnen3lem  43738  onexlimgt  43950  grumnudlem  44975  dvconstbi  45024  expgrowth  45025  eliuniin  45797  wessf1ornlem  45883  ssmapsn  45912  limccog  46316  0ellimcdiv  46343  cosknegpi  46563  cncfshift  46568  cncfperiod  46573  cncfuni  46580  icccncfext  46581  dvbdfbdioolem1  46622  itgperiod  46675  stoweidlem57  46751  fourierdlem12  46813  fourierdlem48  46848  fourierdlem49  46849  fourierdlem52  46852  fourierdlem54  46854  fourierdlem68  46868  fourierdlem77  46877  fourierdlem83  46883  fourierdlem87  46887  fourierdlem102  46902  fourierdlem103  46903  fourierdlem104  46904  fourierdlem113  46913  fourierdlem114  46914  elaa2  46928  etransclem24  46952  etransclem32  46960  etransclem48  46976  ovolval5lem3  47348  sssmf  47432  sigarcol  47558  f1oresf1o2  48005  imaelsetpreimafv  48121  uhgrimisgrgriclem  48672