Theorem rexlimdv3a 3137

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

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2111  ∃wrex 3056

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 1911

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

This theorem is referenced by:  sorpssuni  7665  sorpssint  7666  mapsnd  8810  tcrank  9774  rpnnen1lem5  12876  hashfun  14341  resqrex  15154  resqrtcl  15157  fprodle  15900  prmgaplem6  16965  lbsextlem3  21095  cmpsublem  23312  cmpcld  23315  ovoliunlem2  25429  isblo3i  30776  trisegint  36061  itg2addnclem  37710  areacirclem2  37748  lshpnelb  39022  lsatfixedN  39047  lsmsatcv  39048  lssatomic  39049  lcv1  39079  lsatcvatlem  39087  islshpcv  39091  lfl1  39108  lshpsmreu  39147  lshpkrex  39156  lshpset2N  39157  lkrlspeqN  39209  cvrval3  39451  1cvratlt  39512  ps-2b  39520  llnnleat  39551  lvolex3N  39576  lplncvrlvol2  39653  osumcllem7N  40000  lhp0lt  40041  lhpj1  40060  4atexlemex6  40112  4atexlem7  40113  trlnidat  40211  cdlemd9  40244  cdleme21h  40372  cdlemg7fvbwN  40645  cdlemg7aN  40663  cdlemg34  40750  cdlemg36  40752  cdlemg44  40771  cdlemg48  40775  tendo1ne0  40866  cdlemk26-3  40944  cdlemk55b  40998  cdleml4N  41017  dih1dimatlem0  41366  dihglblem6  41378  dochshpncl  41422  dvh4dimlem  41481  dvh3dim2  41486  dvh3dim3N  41487  dochsatshpb  41490  dochexmidlem4  41501  dochexmidlem5  41502  dochexmidlem8  41505  dochkr1  41516  dochkr1OLDN  41517  lcfl7lem  41537  lcfl6  41538  lcfl8  41540  lcfrlem16  41596  lcfrlem40  41620  mapdval2N  41668  mapdrvallem2  41683  mapdpglem24  41742  mapdh6iN  41782  mapdh8ad  41817  mapdh8e  41822  hdmap1l6i  41856  hdmapval0  41871  hdmapevec  41873  hdmapval3N  41876  hdmap10lem  41877  hdmap11lem2  41880  hdmaprnlem15N  41899  hdmaprnlem16N  41900  hdmap14lem10  41915  hdmap14lem11  41916  hdmap14lem12  41917  hdmap14lem14  41919  hgmapval0  41930  hgmapval1  41931  hgmapadd  41932  hgmapmul  41933  hgmaprnlem3N  41936  hgmaprnlem4N  41937  hgmap11  41940  hgmapvvlem3  41963  rpnnen3lem  43063  onexlimgt  43275  grumnudlem  44317  dvconstbi  44366  expgrowth  44367  eliuniin  45135  wessf1ornlem  45221  ssmapsn  45252  limccog  45659  0ellimcdiv  45686  cosknegpi  45906  cncfshift  45911  cncfperiod  45916  cncfuni  45923  icccncfext  45924  dvbdfbdioolem1  45965  itgperiod  46018  stoweidlem57  46094  fourierdlem12  46156  fourierdlem48  46191  fourierdlem49  46192  fourierdlem52  46195  fourierdlem54  46197  fourierdlem68  46211  fourierdlem77  46220  fourierdlem83  46226  fourierdlem87  46230  fourierdlem102  46245  fourierdlem103  46246  fourierdlem104  46247  fourierdlem113  46256  fourierdlem114  46257  elaa2  46271  etransclem24  46295  etransclem32  46303  etransclem48  46319  ovolval5lem3  46691  sigarcol  46901  f1oresf1o2  47321  imaelsetpreimafv  47425  uhgrimisgrgriclem  47960