Theorem rexlimdv3a 3171

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

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

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 1945

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

This theorem is used by:  sorpssuni  7775  sorpssint  7776  mapsnd  8945  tcrank  9931  rpnnen1lem5  13139  hashfun  14612  resqrex  15449  resqrtcl  15452  fprodle  16195  prmgaplem6  17266  lbsextlem3  21471  cmpsublem  23750  cmpcld  23753  ovoliunlem2  25857  isblo3i  31436  trisegint  36984  itg2addnclem  38794  areacirclem2  38832  lshpnelb  40244  lsatfixedN  40269  lsmsatcv  40270  lssatomic  40271  lcv1  40301  lsatcvatlem  40309  islshpcv  40313  lfl1  40330  lshpsmreu  40369  lshpkrex  40378  lshpset2N  40379  lkrlspeqN  40431  cvrval3  40673  1cvratlt  40734  ps-2b  40742  llnnleat  40773  lvolex3N  40798  lplncvrlvol2  40875  osumcllem7N  41222  lhp0lt  41263  lhpj1  41282  4atexlemex6  41334  4atexlem7  41335  trlnidat  41433  cdlemd9  41466  cdleme21h  41594  cdlemg7fvbwN  41867  cdlemg7aN  41885  cdlemg34  41972  cdlemg36  41974  cdlemg44  41993  cdlemg48  41997  tendo1ne0  42088  cdlemk26-3  42166  cdlemk55b  42220  cdleml4N  42239  dih1dimatlem0  42588  dihglblem6  42600  dochshpncl  42644  dvh4dimlem  42703  dvh3dim2  42708  dvh3dim3N  42709  dochsatshpb  42712  dochexmidlem4  42723  dochexmidlem5  42724  dochexmidlem8  42727  dochkr1  42738  dochkr1OLDN  42739  lcfl7lem  42759  lcfl6  42760  lcfl8  42762  lcfrlem16  42818  lcfrlem40  42842  mapdval2N  42890  mapdrvallem2  42905  mapdpglem24  42964  mapdh6iN  43004  mapdh8ad  43039  mapdh8e  43044  hdmap1l6i  43078  hdmapval0  43093  hdmapevec  43095  hdmapval3N  43098  hdmap10lem  43099  hdmap11lem2  43102  hdmaprnlem15N  43121  hdmaprnlem16N  43122  hdmap14lem10  43137  hdmap14lem11  43138  hdmap14lem12  43139  hdmap14lem14  43141  hgmapval0  43152  hgmapval1  43153  hgmapadd  43154  hgmapmul  43155  hgmaprnlem3N  43158  hgmaprnlem4N  43159  hgmap11  43162  hgmapvvlem3  43185  rpnnen3lem  44242  onexlimgt  44448  grumnudlem  45472  dvconstbi  45521  expgrowth  45522  eliuniin  46329  wessf1ornlem  46415  ssmapsn  46444  limccog  46847  0ellimcdiv  46874  cosknegpi  47094  cncfshift  47099  cncfperiod  47104  cncfuni  47111  icccncfext  47112  dvbdfbdioolem1  47153  itgperiod  47206  stoweidlem57  47282  fourierdlem12  47344  fourierdlem48  47379  fourierdlem49  47380  fourierdlem52  47383  fourierdlem54  47385  fourierdlem68  47399  fourierdlem77  47408  fourierdlem83  47414  fourierdlem87  47418  fourierdlem102  47433  fourierdlem103  47434  fourierdlem104  47435  fourierdlem113  47444  fourierdlem114  47445  elaa2  47459  etransclem24  47483  etransclem32  47491  etransclem48  47507  ovolval5lem3  47879  sssmf  47963  sigarcol  48089  f1oresf1o2  48576  imaelsetpreimafv  48692  uhgrimisgrgriclem  49243