Theorem rexlimdv3a 3169

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

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

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 3089

This theorem is used by:  sorpssuni  7737  sorpssint  7738  mapsnd  8897  tcrank  9870  rpnnen1lem5  13035  hashfun  14506  resqrex  15341  resqrtcl  15344  fprodle  16089  prmgaplem6  17154  lbsextlem3  21353  cmpsublem  23630  cmpcld  23633  ovoliunlem2  25737  isblo3i  31290  trisegint  36616  itg2addnclem  38428  areacirclem2  38466  lshpnelb  39865  lsatfixedN  39890  lsmsatcv  39891  lssatomic  39892  lcv1  39922  lsatcvatlem  39930  islshpcv  39934  lfl1  39951  lshpsmreu  39990  lshpkrex  39999  lshpset2N  40000  lkrlspeqN  40052  cvrval3  40294  1cvratlt  40355  ps-2b  40363  llnnleat  40394  lvolex3N  40419  lplncvrlvol2  40496  osumcllem7N  40843  lhp0lt  40884  lhpj1  40903  4atexlemex6  40955  4atexlem7  40956  trlnidat  41054  cdlemd9  41087  cdleme21h  41215  cdlemg7fvbwN  41488  cdlemg7aN  41506  cdlemg34  41593  cdlemg36  41595  cdlemg44  41614  cdlemg48  41618  tendo1ne0  41709  cdlemk26-3  41787  cdlemk55b  41841  cdleml4N  41860  dih1dimatlem0  42209  dihglblem6  42221  dochshpncl  42265  dvh4dimlem  42324  dvh3dim2  42329  dvh3dim3N  42330  dochsatshpb  42333  dochexmidlem4  42344  dochexmidlem5  42345  dochexmidlem8  42348  dochkr1  42359  dochkr1OLDN  42360  lcfl7lem  42380  lcfl6  42381  lcfl8  42383  lcfrlem16  42439  lcfrlem40  42463  mapdval2N  42511  mapdrvallem2  42526  mapdpglem24  42585  mapdh6iN  42625  mapdh8ad  42660  mapdh8e  42665  hdmap1l6i  42699  hdmapval0  42714  hdmapevec  42716  hdmapval3N  42719  hdmap10lem  42720  hdmap11lem2  42723  hdmaprnlem15N  42742  hdmaprnlem16N  42743  hdmap14lem10  42758  hdmap14lem11  42759  hdmap14lem12  42760  hdmap14lem14  42762  hgmapval0  42773  hgmapval1  42774  hgmapadd  42775  hgmapmul  42776  hgmaprnlem3N  42779  hgmaprnlem4N  42780  hgmap11  42783  hgmapvvlem3  42806  rpnnen3lem  43880  onexlimgt  44092  grumnudlem  45117  dvconstbi  45166  expgrowth  45167  eliuniin  45939  wessf1ornlem  46025  ssmapsn  46054  limccog  46458  0ellimcdiv  46485  cosknegpi  46705  cncfshift  46710  cncfperiod  46715  cncfuni  46722  icccncfext  46723  dvbdfbdioolem1  46764  itgperiod  46817  stoweidlem57  46893  fourierdlem12  46955  fourierdlem48  46990  fourierdlem49  46991  fourierdlem52  46994  fourierdlem54  46996  fourierdlem68  47010  fourierdlem77  47019  fourierdlem83  47025  fourierdlem87  47029  fourierdlem102  47044  fourierdlem103  47045  fourierdlem104  47046  fourierdlem113  47055  fourierdlem114  47056  elaa2  47070  etransclem24  47094  etransclem32  47102  etransclem48  47118  ovolval5lem3  47490  sssmf  47574  sigarcol  47700  f1oresf1o2  48187  imaelsetpreimafv  48303  uhgrimisgrgriclem  48854