Theorem rexlimdv3a 3168

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

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

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 3088

This theorem is used by:  sorpssuni  7737  sorpssint  7738  mapsnd  8898  tcrank  9882  rpnnen1lem5  13090  hashfun  14562  resqrex  15397  resqrtcl  15400  fprodle  16143  prmgaplem6  17214  lbsextlem3  21418  cmpsublem  23697  cmpcld  23700  ovoliunlem2  25804  isblo3i  31385  trisegint  36763  itg2addnclem  38557  areacirclem2  38595  lshpnelb  40009  lsatfixedN  40034  lsmsatcv  40035  lssatomic  40036  lcv1  40066  lsatcvatlem  40074  islshpcv  40078  lfl1  40095  lshpsmreu  40134  lshpkrex  40143  lshpset2N  40144  lkrlspeqN  40196  cvrval3  40438  1cvratlt  40499  ps-2b  40507  llnnleat  40538  lvolex3N  40563  lplncvrlvol2  40640  osumcllem7N  40987  lhp0lt  41028  lhpj1  41047  4atexlemex6  41099  4atexlem7  41100  trlnidat  41198  cdlemd9  41231  cdleme21h  41359  cdlemg7fvbwN  41632  cdlemg7aN  41650  cdlemg34  41737  cdlemg36  41739  cdlemg44  41758  cdlemg48  41762  tendo1ne0  41853  cdlemk26-3  41931  cdlemk55b  41985  cdleml4N  42004  dih1dimatlem0  42353  dihglblem6  42365  dochshpncl  42409  dvh4dimlem  42468  dvh3dim2  42473  dvh3dim3N  42474  dochsatshpb  42477  dochexmidlem4  42488  dochexmidlem5  42489  dochexmidlem8  42492  dochkr1  42503  dochkr1OLDN  42504  lcfl7lem  42524  lcfl6  42525  lcfl8  42527  lcfrlem16  42583  lcfrlem40  42607  mapdval2N  42655  mapdrvallem2  42670  mapdpglem24  42729  mapdh6iN  42769  mapdh8ad  42804  mapdh8e  42809  hdmap1l6i  42843  hdmapval0  42858  hdmapevec  42860  hdmapval3N  42863  hdmap10lem  42864  hdmap11lem2  42867  hdmaprnlem15N  42886  hdmaprnlem16N  42887  hdmap14lem10  42902  hdmap14lem11  42903  hdmap14lem12  42904  hdmap14lem14  42906  hgmapval0  42917  hgmapval1  42918  hgmapadd  42919  hgmapmul  42920  hgmaprnlem3N  42923  hgmaprnlem4N  42924  hgmap11  42927  hgmapvvlem3  42950  rpnnen3lem  43991  onexlimgt  44203  grumnudlem  45228  dvconstbi  45277  expgrowth  45278  eliuniin  46057  wessf1ornlem  46143  ssmapsn  46172  limccog  46576  0ellimcdiv  46603  cosknegpi  46823  cncfshift  46828  cncfperiod  46833  cncfuni  46840  icccncfext  46841  dvbdfbdioolem1  46882  itgperiod  46935  stoweidlem57  47011  fourierdlem12  47073  fourierdlem48  47108  fourierdlem49  47109  fourierdlem52  47112  fourierdlem54  47114  fourierdlem68  47128  fourierdlem77  47137  fourierdlem83  47143  fourierdlem87  47147  fourierdlem102  47162  fourierdlem103  47163  fourierdlem104  47164  fourierdlem113  47173  fourierdlem114  47174  elaa2  47188  etransclem24  47212  etransclem32  47220  etransclem48  47236  ovolval5lem3  47608  sssmf  47692  sigarcol  47818  f1oresf1o2  48305  imaelsetpreimafv  48421  uhgrimisgrgriclem  48972