Theorem rexlimdv3a 3138

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

Syntax hints:   → wi 4   ∧ w3a 1086   ∈ wcel 2113  ∃wrex 3057

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 3058

This theorem is referenced by:  sorpssuni  7671  sorpssint  7672  mapsnd  8816  tcrank  9784  rpnnen1lem5  12881  hashfun  14346  resqrex  15159  resqrtcl  15162  fprodle  15905  prmgaplem6  16970  lbsextlem3  21099  cmpsublem  23315  cmpcld  23318  ovoliunlem2  25432  isblo3i  30783  trisegint  36093  itg2addnclem  37731  areacirclem2  37769  lshpnelb  39103  lsatfixedN  39128  lsmsatcv  39129  lssatomic  39130  lcv1  39160  lsatcvatlem  39168  islshpcv  39172  lfl1  39189  lshpsmreu  39228  lshpkrex  39237  lshpset2N  39238  lkrlspeqN  39290  cvrval3  39532  1cvratlt  39593  ps-2b  39601  llnnleat  39632  lvolex3N  39657  lplncvrlvol2  39734  osumcllem7N  40081  lhp0lt  40122  lhpj1  40141  4atexlemex6  40193  4atexlem7  40194  trlnidat  40292  cdlemd9  40325  cdleme21h  40453  cdlemg7fvbwN  40726  cdlemg7aN  40744  cdlemg34  40831  cdlemg36  40833  cdlemg44  40852  cdlemg48  40856  tendo1ne0  40947  cdlemk26-3  41025  cdlemk55b  41079  cdleml4N  41098  dih1dimatlem0  41447  dihglblem6  41459  dochshpncl  41503  dvh4dimlem  41562  dvh3dim2  41567  dvh3dim3N  41568  dochsatshpb  41571  dochexmidlem4  41582  dochexmidlem5  41583  dochexmidlem8  41586  dochkr1  41597  dochkr1OLDN  41598  lcfl7lem  41618  lcfl6  41619  lcfl8  41621  lcfrlem16  41677  lcfrlem40  41701  mapdval2N  41749  mapdrvallem2  41764  mapdpglem24  41823  mapdh6iN  41863  mapdh8ad  41898  mapdh8e  41903  hdmap1l6i  41937  hdmapval0  41952  hdmapevec  41954  hdmapval3N  41957  hdmap10lem  41958  hdmap11lem2  41961  hdmaprnlem15N  41980  hdmaprnlem16N  41981  hdmap14lem10  41996  hdmap14lem11  41997  hdmap14lem12  41998  hdmap14lem14  42000  hgmapval0  42011  hgmapval1  42012  hgmapadd  42013  hgmapmul  42014  hgmaprnlem3N  42017  hgmaprnlem4N  42018  hgmap11  42021  hgmapvvlem3  42044  rpnnen3lem  43148  onexlimgt  43360  grumnudlem  44402  dvconstbi  44451  expgrowth  44452  eliuniin  45220  wessf1ornlem  45306  ssmapsn  45337  limccog  45744  0ellimcdiv  45771  cosknegpi  45991  cncfshift  45996  cncfperiod  46001  cncfuni  46008  icccncfext  46009  dvbdfbdioolem1  46050  itgperiod  46103  stoweidlem57  46179  fourierdlem12  46241  fourierdlem48  46276  fourierdlem49  46277  fourierdlem52  46280  fourierdlem54  46282  fourierdlem68  46296  fourierdlem77  46305  fourierdlem83  46311  fourierdlem87  46315  fourierdlem102  46330  fourierdlem103  46331  fourierdlem104  46332  fourierdlem113  46341  fourierdlem114  46342  elaa2  46356  etransclem24  46380  etransclem32  46388  etransclem48  46404  ovolval5lem3  46776  sigarcol  46986  f1oresf1o2  47415  imaelsetpreimafv  47519  uhgrimisgrgriclem  48054