Theorem rexlimd 3239

Description: Deduction form of rexlimd 3239. For a version based on fewer axioms see rexlimdv 3131. (Contributed by NM, 27-May-1998.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 14-Jan-2020.)

Hypotheses

Ref	Expression
rexlimd.1	⊢ Ⅎ𝑥𝜑
rexlimd.2	⊢ Ⅎ𝑥𝜒
rexlimd.3	⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))

Assertion

Ref	Expression
rexlimd	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Proof of Theorem rexlimd

Step	Hyp	Ref	Expression
1		rexlimd.1	. 2 ⊢ Ⅎ𝑥𝜑
2		rexlimd.2	. . 3 ⊢ Ⅎ𝑥𝜒
3	2	a1i 11	. 2 ⊢ (𝜑 → Ⅎ𝑥𝜒)
4		rexlimd.3	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
5	1, 3, 4	rexlimd2 3238	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4  Ⅎwnf 1784   ∈ wcel 2111  ∃wrex 3056

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  ax-6 1968  ax-7 2009  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-ral 3048  df-rex 3057

This theorem is referenced by:  r19.29af2  3240  iuneqconst  4953  reusv2lem2  5337  ralxfrALT  5353  funimassd  6888  fvelimad  6889  fvmptt  6949  dffo3f  7039  ffnfv  7052  frpoins3xpg  8070  frpoins3xp3g  8071  tz7.49  8364  nneneq  9115  ac6sfi  9168  ixpiunwdom  9476  r1val1  9676  rankuni2b  9743  infpssrlem4  10194  zorn2lem4  10387  zorn2lem5  10388  konigthlem  10456  tskuni  10671  gruiin  10698  lbzbi  12831  reuccatpfxs1  14651  iunconnlem  23340  ptbasfi  23494  alexsubALTlem3  23962  ovoliunnul  25433  iunmbl2  25483  mptelee  28871  atom1d  32328  elabreximd  32485  iundisjf  32564  esumc  34059  fvineqsneu  37444  poimirlem24  37683  poimirlem26  37685  poimirlem27  37686  heicant  37694  indexa  37772  sdclem2  37781  glbconxN  39416  cdleme26ee  40398  cdleme32d  40482  cdleme32f  40484  cdlemk38  40953  cdlemk19x  40981  cdlemk11t  40984  unielss  43250  oaun3lem1  43406  refsumcn  45066  eliuniin2  45156  rexlimd3  45180  suprnmpt  45210  disjf1o  45227  disjinfi  45228  rnmptlb  45279  rnmptbddlem  45280  rnmptbd2lem  45284  infnsuprnmpt  45286  upbdrech  45345  ssfiunibd  45349  iuneqfzuzlem  45372  infrpge  45389  xrralrecnnle  45420  supxrleubrnmpt  45443  infleinf2  45451  suprleubrnmpt  45459  infrnmptle  45460  infxrunb3rnmpt  45465  infxrgelbrnmpt  45491  iccshift  45557  iooshift  45561  fmul01lt1  45625  islptre  45658  rexlim2d  45664  limcperiod  45667  islpcn  45676  limclner  45688  fnlimfvre  45711  climinf2lem  45743  limsupmnflem  45757  limsupre3uzlem  45772  climuzlem  45780  dvnprodlem1  45983  dvnprodlem2  45984  itgperiod  46018  stoweidlem29  46066  stoweidlem31  46068  stoweidlem59  46096  stirlinglem13  46123  fourierdlem48  46191  fourierdlem51  46194  fourierdlem80  46223  fourierdlem81  46224  fourierdlem93  46236  elaa2  46271  salexct  46371  sge00  46413  sge0f1o  46419  sge0gerp  46432  sge0lefi  46435  sge0ltfirp  46437  sge0resplit  46443  sge0iunmptlemre  46452  sge0iunmpt  46455  sge0isum  46464  sge0xp  46466  sge0reuz  46484  sge0reuzb  46485  iundjiun  46497  voliunsge0lem  46509  meaiuninc3v  46521  meaiininc2  46525  isomenndlem  46567  ovncvrrp  46601  ovnsubaddlem1  46607  hoidmvval0  46624  hoidmvlelem1  46632  vonioo  46719  vonicc  46722  smfaddlem1  46800  smfresal  46825  smfpimbor1lem2  46836  smflimmpt  46847  smfinflem  46854  smflimsuplem7  46863  smflimsuplem8  46864  smflimsupmpt  46866  smfliminfmpt  46869  ffnafv  47201  f1oresf1o2  47321  iccpartdisj  47467  mogoldbb  47815  2zrngagrp  48279  iunord  49707