Theorem rexlimdv3a 3145

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

Syntax hints:   → wi 4   ∧ w3a 1092   ∈ wcel 2119  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-ex 1787  df-rex 3065

This theorem is referenced by:  sorpssuni  7682  sorpssint  7683  mapsnd  8831  tcrank  9806  rpnnen1lem5  12929  hashfun  14397  resqrex  15210  resqrtcl  15213  fprodle  15959  prmgaplem6  17025  lbsextlem3  21160  cmpsublem  23389  cmpcld  23392  ovoliunlem2  25495  isblo3i  30897  trisegint  36263  itg2addnclem  38045  areacirclem2  38083  lshpnelb  39483  lsatfixedN  39508  lsmsatcv  39509  lssatomic  39510  lcv1  39540  lsatcvatlem  39548  islshpcv  39552  lfl1  39569  lshpsmreu  39608  lshpkrex  39617  lshpset2N  39618  lkrlspeqN  39670  cvrval3  39912  1cvratlt  39973  ps-2b  39981  llnnleat  40012  lvolex3N  40037  lplncvrlvol2  40114  osumcllem7N  40461  lhp0lt  40502  lhpj1  40521  4atexlemex6  40573  4atexlem7  40574  trlnidat  40672  cdlemd9  40705  cdleme21h  40833  cdlemg7fvbwN  41106  cdlemg7aN  41124  cdlemg34  41211  cdlemg36  41213  cdlemg44  41232  cdlemg48  41236  tendo1ne0  41327  cdlemk26-3  41405  cdlemk55b  41459  cdleml4N  41478  dih1dimatlem0  41827  dihglblem6  41839  dochshpncl  41883  dvh4dimlem  41942  dvh3dim2  41947  dvh3dim3N  41948  dochsatshpb  41951  dochexmidlem4  41962  dochexmidlem5  41963  dochexmidlem8  41966  dochkr1  41977  dochkr1OLDN  41978  lcfl7lem  41998  lcfl6  41999  lcfl8  42001  lcfrlem16  42057  lcfrlem40  42081  mapdval2N  42129  mapdrvallem2  42144  mapdpglem24  42203  mapdh6iN  42243  mapdh8ad  42278  mapdh8e  42283  hdmap1l6i  42317  hdmapval0  42332  hdmapevec  42334  hdmapval3N  42337  hdmap10lem  42338  hdmap11lem2  42341  hdmaprnlem15N  42360  hdmaprnlem16N  42361  hdmap14lem10  42376  hdmap14lem11  42377  hdmap14lem12  42378  hdmap14lem14  42380  hgmapval0  42391  hgmapval1  42392  hgmapadd  42393  hgmapmul  42394  hgmaprnlem3N  42397  hgmaprnlem4N  42398  hgmap11  42401  hgmapvvlem3  42424  rpnnen3lem  43483  onexlimgt  43695  grumnudlem  44736  dvconstbi  44785  expgrowth  44786  eliuniin  45553  wessf1ornlem  45639  ssmapsn  45668  limccog  46072  0ellimcdiv  46099  cosknegpi  46319  cncfshift  46324  cncfperiod  46329  cncfuni  46336  icccncfext  46337  dvbdfbdioolem1  46378  itgperiod  46431  stoweidlem57  46507  fourierdlem12  46569  fourierdlem48  46604  fourierdlem49  46605  fourierdlem52  46608  fourierdlem54  46610  fourierdlem68  46624  fourierdlem77  46633  fourierdlem83  46639  fourierdlem87  46643  fourierdlem102  46658  fourierdlem103  46659  fourierdlem104  46660  fourierdlem113  46669  fourierdlem114  46670  elaa2  46684  etransclem24  46708  etransclem32  46716  etransclem48  46732  ovolval5lem3  47104  sigarcol  47314  f1oresf1o2  47761  imaelsetpreimafv  47877  uhgrimisgrgriclem  48428