Theorem rexlimdv3a 3144

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

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

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 3064

This theorem is referenced by:  sorpssuni  7676  sorpssint  7677  mapsnd  8825  tcrank  9800  rpnnen1lem5  12923  hashfun  14391  resqrex  15204  resqrtcl  15207  fprodle  15953  prmgaplem6  17019  lbsextlem3  21154  cmpsublem  23383  cmpcld  23386  ovoliunlem2  25489  isblo3i  30891  trisegint  36265  itg2addnclem  38047  areacirclem2  38085  lshpnelb  39485  lsatfixedN  39510  lsmsatcv  39511  lssatomic  39512  lcv1  39542  lsatcvatlem  39550  islshpcv  39554  lfl1  39571  lshpsmreu  39610  lshpkrex  39619  lshpset2N  39620  lkrlspeqN  39672  cvrval3  39914  1cvratlt  39975  ps-2b  39983  llnnleat  40014  lvolex3N  40039  lplncvrlvol2  40116  osumcllem7N  40463  lhp0lt  40504  lhpj1  40523  4atexlemex6  40575  4atexlem7  40576  trlnidat  40674  cdlemd9  40707  cdleme21h  40835  cdlemg7fvbwN  41108  cdlemg7aN  41126  cdlemg34  41213  cdlemg36  41215  cdlemg44  41234  cdlemg48  41238  tendo1ne0  41329  cdlemk26-3  41407  cdlemk55b  41461  cdleml4N  41480  dih1dimatlem0  41829  dihglblem6  41841  dochshpncl  41885  dvh4dimlem  41944  dvh3dim2  41949  dvh3dim3N  41950  dochsatshpb  41953  dochexmidlem4  41964  dochexmidlem5  41965  dochexmidlem8  41968  dochkr1  41979  dochkr1OLDN  41980  lcfl7lem  42000  lcfl6  42001  lcfl8  42003  lcfrlem16  42059  lcfrlem40  42083  mapdval2N  42131  mapdrvallem2  42146  mapdpglem24  42205  mapdh6iN  42245  mapdh8ad  42280  mapdh8e  42285  hdmap1l6i  42319  hdmapval0  42334  hdmapevec  42336  hdmapval3N  42339  hdmap10lem  42340  hdmap11lem2  42343  hdmaprnlem15N  42362  hdmaprnlem16N  42363  hdmap14lem10  42378  hdmap14lem11  42379  hdmap14lem12  42380  hdmap14lem14  42382  hgmapval0  42393  hgmapval1  42394  hgmapadd  42395  hgmapmul  42396  hgmaprnlem3N  42399  hgmaprnlem4N  42400  hgmap11  42403  hgmapvvlem3  42426  rpnnen3lem  43485  onexlimgt  43697  grumnudlem  44738  dvconstbi  44787  expgrowth  44788  eliuniin  45554  wessf1ornlem  45640  ssmapsn  45669  limccog  46073  0ellimcdiv  46100  cosknegpi  46320  cncfshift  46325  cncfperiod  46330  cncfuni  46337  icccncfext  46338  dvbdfbdioolem1  46379  itgperiod  46432  stoweidlem57  46508  fourierdlem12  46570  fourierdlem48  46605  fourierdlem49  46606  fourierdlem52  46609  fourierdlem54  46611  fourierdlem68  46625  fourierdlem77  46634  fourierdlem83  46640  fourierdlem87  46644  fourierdlem102  46659  fourierdlem103  46660  fourierdlem104  46661  fourierdlem113  46670  fourierdlem114  46671  elaa2  46685  etransclem24  46709  etransclem32  46717  etransclem48  46733  ovolval5lem3  47105  sigarcol  47315  f1oresf1o2  47762  imaelsetpreimafv  47878  uhgrimisgrgriclem  48429