Theorem rexlimdv3a 3167

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

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

This theorem is used by:  sorpssuni  7749  sorpssint  7750  mapsnd  8918  tcrank  9905  rpnnen1lem5  13113  hashfun  14586  resqrex  15423  resqrtcl  15426  fprodle  16169  prmgaplem6  17240  lbsextlem3  21444  cmpsublem  23723  cmpcld  23726  ovoliunlem2  25830  isblo3i  31409  trisegint  36886  itg2addnclem  38683  areacirclem2  38721  lshpnelb  40135  lsatfixedN  40160  lsmsatcv  40161  lssatomic  40162  lcv1  40192  lsatcvatlem  40200  islshpcv  40204  lfl1  40221  lshpsmreu  40260  lshpkrex  40269  lshpset2N  40270  lkrlspeqN  40322  cvrval3  40564  1cvratlt  40625  ps-2b  40633  llnnleat  40664  lvolex3N  40689  lplncvrlvol2  40766  osumcllem7N  41113  lhp0lt  41154  lhpj1  41173  4atexlemex6  41225  4atexlem7  41226  trlnidat  41324  cdlemd9  41357  cdleme21h  41485  cdlemg7fvbwN  41758  cdlemg7aN  41776  cdlemg34  41863  cdlemg36  41865  cdlemg44  41884  cdlemg48  41888  tendo1ne0  41979  cdlemk26-3  42057  cdlemk55b  42111  cdleml4N  42130  dih1dimatlem0  42479  dihglblem6  42491  dochshpncl  42535  dvh4dimlem  42594  dvh3dim2  42599  dvh3dim3N  42600  dochsatshpb  42603  dochexmidlem4  42614  dochexmidlem5  42615  dochexmidlem8  42618  dochkr1  42629  dochkr1OLDN  42630  lcfl7lem  42650  lcfl6  42651  lcfl8  42653  lcfrlem16  42709  lcfrlem40  42733  mapdval2N  42781  mapdrvallem2  42796  mapdpglem24  42855  mapdh6iN  42895  mapdh8ad  42930  mapdh8e  42935  hdmap1l6i  42969  hdmapval0  42984  hdmapevec  42986  hdmapval3N  42989  hdmap10lem  42990  hdmap11lem2  42993  hdmaprnlem15N  43012  hdmaprnlem16N  43013  hdmap14lem10  43028  hdmap14lem11  43029  hdmap14lem12  43030  hdmap14lem14  43032  hgmapval0  43043  hgmapval1  43044  hgmapadd  43045  hgmapmul  43046  hgmaprnlem3N  43049  hgmaprnlem4N  43050  hgmap11  43053  hgmapvvlem3  43076  rpnnen3lem  44132  onexlimgt  44339  grumnudlem  45363  dvconstbi  45412  expgrowth  45413  eliuniin  46208  wessf1ornlem  46294  ssmapsn  46323  limccog  46726  0ellimcdiv  46753  cosknegpi  46973  cncfshift  46978  cncfperiod  46983  cncfuni  46990  icccncfext  46991  dvbdfbdioolem1  47032  itgperiod  47085  stoweidlem57  47161  fourierdlem12  47223  fourierdlem48  47258  fourierdlem49  47259  fourierdlem52  47262  fourierdlem54  47264  fourierdlem68  47278  fourierdlem77  47287  fourierdlem83  47293  fourierdlem87  47297  fourierdlem102  47312  fourierdlem103  47313  fourierdlem104  47314  fourierdlem113  47323  fourierdlem114  47324  elaa2  47338  etransclem24  47362  etransclem32  47370  etransclem48  47386  ovolval5lem3  47758  sssmf  47842  sigarcol  47968  f1oresf1o2  48455  imaelsetpreimafv  48571  uhgrimisgrgriclem  49122